Детальная информация
| Название | Применение временной логики при верификации процессов обработки и хранения больших данных // Промышленный искусственный интеллект (ПИИ'2025): Всероссийская научно-практическая конференция с международным участием 3–4 июля 2025 года: cборник научных трудов |
|---|---|
| Авторы | Подоров Андрей Алексеевич ; Полтавцева Мария Анатольевна |
| Организация | Санкт-Петербургский политехнический университет Петра Великого |
| Выходные сведения | Санкт-Петербург: ПОЛИТЕХ-ПРЕСС, 2025 |
| Коллекция | Общая коллекция |
| Тип документа | Статья, доклад |
| Язык | Русский |
| DOI | 10.18720/SPBPU/2/id25-557 |
| Права доступа | Доступ по паролю из сети Интернет (чтение, печать, копирование) |
| Дополнительно | Новинка |
| Ключ записи | RU\SPSTU\edoc\77916 |
| Дата создания записи | 26.12.2025 |
Разрешенные действия
–
Действие 'Прочитать' будет доступно, если вы выполните вход в систему или будете работать с сайтом на компьютере в другой сети
Действие 'Загрузить' будет доступно, если вы выполните вход в систему или будете работать с сайтом на компьютере в другой сети
| Группа | Анонимные пользователи |
|---|---|
| Сеть | Интернет |
Тема работы – применение временной логики для верификации систем обработки и хранения больших данных, с целью выявления ошибок и несоответствий в процессах обработки и хранения данных в распределённых системах больших данных. Объектом исследования является распределённая система обработки и хранения больших данных. В работеыл выполнен анализ архитектур и подходов к обеспечению безопасности в распределённых системах, обоснован выбор логики линейного времени и инструмента TLA+, предложена формализация модели жизненного цикла обработки больших данных. Разработан тестовый стенд, выполняющий автоматическую генерацию спецификаций на языке TLA+.
The topic of the paper is the application of temporal logic for verification of big data processing and storage systems, in order to identify errors and inconsistencies in the processes of data processing and storage in distributed big data systems. The object of the research is a distributed big data processing and storage system. The paper analyzes architectures and approaches to ensuring security in distributed systems, justifies the choice of linear time logic and the TLA+ tool, and formalizes the life cycle model for big data processing. A test bench has been developed that performs automatic specification generation in the TLA+ language.
| Место доступа | Группа пользователей | Действие |
|---|---|---|
| Локальная сеть ИБК СПбПУ | Все |
|
| Интернет | Авторизованные пользователи СПбПУ |
|
| Интернет | Анонимные пользователи |
|
Количество обращений: 0
За последние 30 дней: 0
