Модели процессов: проверка соответствия наблюдаемому поведению, автоматический синтез и анализ поведенческих свойств

В научно-учебной лаборатории процессно-ориентированных информационных систем (ПОИС) в 2021 году велась научно-исследовательская работа над новыми алгоритмами верификации автоматных моделей программ и оценкой сложности этих алгоритмов, а также над новыми подходами к построению моделей поведения распределенных информационных систем. Кроме того, разработаны новые подходы к проверке соответствия между поведением процессов, которое допускается их формальными моделями, и журналами событий, содержащими наблюдаемое поведение процессов. Среди основных результатов по направлению верификации автоматных моделей программ выделим следующие: алгоритм проверки формул логики Reg-LTL с помощью автоматов Бюхи специального вида и доказательство его принадлежности к классу PSPACE-полных задач по емкостной сложности; алгоритм строгой проверки детерминированности автоматов реального времени и доказательство его принадлежности к классу co-NP-полных задач по временной сложности. Среди основных результатов по разработке новых подходов к построению моделей поведения распределенных информационных систем, а также его анализу на основе журналов событий выделим следующие: расширение формализма сетей Петри для моделирования мультиагентных систем с синхронно взаимодействующими агентами и длительными действиями (DaHL-сети); алгоритм построения гибридного графа достижимости для DaHL-сетей; формальные модели шаблонов типичного синхронного и асинхронного взаимодействия агентов в мультиагентных системах; алгоритмы генерации тестовых наборов сетей Петри, обладающих заданными структурными и поведенческими свойствами; алгоритм проверки соответствия между поведением раскрашенной сети Петри и данными из журнала событий; алгоритм представления и анализа информации из журналов событий с применением баз данных; метод анализа производительности информационных систем на основе расширения сетей Петри, в котором моделируются операции обработки совместно используемых данных; выделение и анализ распространенности основных архитектурных стилей разработки программного обеспечения.