Методы синтеза, исправления, проверки соответствия и анализа моделей процессов и распределенных информационных систем

Цель: разработка и исследование новых методов анализа и верификации автоматных моделей информационных систем, а также новых подходов к симуляции, визуализации, синтезу, исправлению и проверке соответствия моделей сложно организованных информационных систем по примерам их наблюдаемого поведения, которое регистрируется в журналах событий. В области анализа и верификации автоматных моделей информационных систем получены следующие результаты: исследована проблема эквивалентности для автоматов-преобразователей, в рамках которой выделен класс префиксных автоматов преобразователей. Показано, что для префиксных автоматов-преобразователей реального времени существует алгоритм проверки эквивалентности, имеющий квадратичную сложность относительно размера автоматов. Также показано, что для префиксных автоматов-преобразователей с эпсилон-переходами существует алгоритм проверки эквивалентности, который имеет кубическую сложность относительно размера автоматов. Дополнительно установлено, что детерминированные двухленточные автоматы транслируются за линейное время в префиксные автоматы-преобразователи. Таким образом, для детерминированных двухленточных автоматов построен алгоритм проверки эквивалентности, имеющий кубическую сложность. Для того чтобы построить описанные алгоритмы, предложен оригинальный метод решения систем линейных языковых уравнений. Исследована задача проверки эквивалентности недетерминированных автоматов-преобразователей, которые работают над унарным выходным алфавитом. Установлено, что в случае, когда проекции автоматов-преобразователей на входной алфавит являются детерминированными автоматами, задача проверки эквивалентности исходных автоматов-преобразователей разрешима. Показано, что задача проверки выполнимости регулярного расширения темпоральной логики деревьев вычислений Reg-CTL* на моделях последовательных реагирующих систем, которые представлены автоматами-преобразователями, является PSPACE-полной. В области симуляции, визуализации, синтеза, исправления и проверки соответствия моделей информационных систем по примерам их наблюдаемого поведения получены следующие результаты: исследована задача сопоставления визуальных моделей информационных систем, представленных в нотации BPMN (Business Process Model and Notation). Для решения этой задачи адаптированы известные эвристические алгоритмы, к которым относятся алгоритм поиска с запретами, муравьиный алгоритм и алгоритм имитации отжига. Показано, что эти алгоритмы позволяют находить минимальные редакционные расстояния между двумя BPMN-моделями. Экспериментально установлено, что время их работы существенно ниже времени работы точного алгоритма нахождения минимального редакционного расстояния. Предложен специальный алгоритм для симуляции моделей процессов в виде расширенных сетей Петри, которые допускают наличие ингибиторных и обнуляющих дуг. Разработанный алгоритм реализован в виде программного инструмента с открытым исходным кодом, которые регистрирует наблюдаемое поведение расширенной сети Петри в журнале событий. Приоритеты срабатывания переходов являются одним из способов управления поведением сетей Петри для обеспечения их живости и ограниченности. Необходимость в них обусловлена ограниченностью ресурсов, характеризующей большинство реальных информационных систем. Реализован предложенный ранее алгоритм вычисления приоритетов срабатывания переходов в сетях Петри. Проведены эксперименты по вычислению приоритетов в моделях сложных распределенных вычислений. Выявлены типичные паттерны асинхронного взаимодействия агентов в сложных мультиагентных системах. Построены формальные модели паттернов в виде композиции сетей Петри, а также изучены их семантические свойства. Показано, как паттерны асинхронного взаимодействия агентов могут применяться для синтеза структурированных моделей мультиагентных систем по журналам событий. Предложен новый метод проверки соответствия между моделями информационных систем и примерами их наблюдаемого поведения из журналов событий, когда допускается не только полное, но и частичное соответствие последовательностей наблюдаемого и моделируемого поведения. В рамках метода предложена специальная метрика оценки соответствия. Усовершенствован разработанный ранее метод декомпозиции моделей в нотации сетей Петри, который используется для исправления фрагментов модели в соответствии с журналами событий и др.