Details
| Title | Применение временной логики при верификации процессов обработки и хранения больших данных // Промышленный искусственный интеллект (ПИИ'2025): Всероссийская научно-практическая конференция с международным участием 3–4 июля 2025 года: cборник научных трудов |
|---|---|
| Creators | Подоров Андрей Алексеевич ; Полтавцева Мария Анатольевна |
| Organization | Санкт-Петербургский политехнический университет Петра Великого |
| Imprint | Санкт-Петербург: ПОЛИТЕХ-ПРЕСС, 2025 |
| Collection | Общая коллекция |
| Document type | Article, report |
| Language | Russian |
| DOI | 10.18720/SPBPU/2/id25-557 |
| Rights | Доступ по паролю из сети Интернет (чтение, печать, копирование) |
| Additionally | New arrival |
| Record key | RU\SPSTU\edoc\77916 |
| Record create date | 12/26/2025 |
Allowed Actions
–
Action 'Read' will be available if you login or access site from another network
Action 'Download' will be available if you login or access site from another network
| Group | Anonymous |
|---|---|
| Network | Internet |
Тема работы – применение временной логики для верификации систем обработки и хранения больших данных, с целью выявления ошибок и несоответствий в процессах обработки и хранения данных в распределённых системах больших данных. Объектом исследования является распределённая система обработки и хранения больших данных. В работеыл выполнен анализ архитектур и подходов к обеспечению безопасности в распределённых системах, обоснован выбор логики линейного времени и инструмента 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.
| Network | User group | Action |
|---|---|---|
| ILC SPbPU Local Network | All |
|
| Internet | Authorized users SPbPU |
|
| Internet | Anonymous |
|
Access count: 0
Last 30 days: 0
