• A
  • A
  • A
  • АБB
  • АБB
  • АБB
  • А
  • А
  • А
  • А
  • А
Обычная версия сайта
Версия для слабовидящихЛичный кабинет сотрудника ВШЭПоиск

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

Приоритетные направления развития: компьютерно-математическое
2019

Цель работы

Разработка и исследование новых методов анализа и верификации автоматных моделей информационных систем, а также новых подходов к симуляции, визуализации, синтезу, исправлению и проверке соответствия моделей сложно организованных информационных систем по примерам их наблюдаемого поведения, которое регистрируется в журналах событий.

Используемые методы

При разработке методов анализа и верификации автоматных моделей информационных систем применяется теория конечных автоматов-преобразователей, а также фрагментов и расширений темпоральной логики деревьев вычислений (CTL). При разработке новых подходов к анализу наблюдаемого поведения информационных систем используется теория формальных языков, сетей Петри и их расширений.

Эмпирическая база исследования

Эмпирической базой исследования служат конкретные примеры распределенных информационных систем и журналы событий, в которых отражается история их функционирования.

Результаты работы

В области анализа и верификации автоматных моделей информационных систем получены следующие результаты:

Исследована проблема эквивалентности для автоматов-преобразователей, в рамках которой выделен класс префиксных автоматов преобразователей. Показано, что для префиксных автоматов-преобразователей реального времени существует алгоритм проверки эквивалентности, имеющий квадратичную сложность относительно размера автоматов. Также показано, что для префиксных автоматов-преобразователей с эпсилон-переходами существует алгоритм проверки эквивалентности, который имеет кубическую сложность относительно размера автоматов. Дополнительно установлено, что детерминированные двухленточные автоматы транслируются за линейное время в префиксные автоматы-преобразователи. Таким образом, для детерминированных двухленточных автоматов построен алгоритм проверки эквивалентности, имеющий кубическую сложность. Для того чтобы построить описанные алгоритмы, был предложен оригинальный метод решения систем линейных языковых уравнений.

Исследована задача проверки эквивалентности недетерминированных автоматов-преобразователей, которые работают над унарным выходным алфавитом. Установлено, что в случае, когда проекции автоматов-преобразователей на входной алфавит являются детерминированными автоматами, задача проверки эквивалентности исходных автоматов-преобразователей разрешима.

Показано, что задача проверки выполнимости регулярного расширения темпоральной логики деревьев вычислений Reg-CTL* на моделях последовательных реагирующих систем, которые представлены автоматами-преобразователями, является PSPACE-полной.

В области симуляции, визуализации, синтеза, исправления и проверки соответствия моделей информационных систем по примерам их наблюдаемого поведения получены следующие результаты:

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

Предложен специальный алгоритм для симуляции моделей процессов в виде расширенных сетей Петри, которые допускают наличие ингибиторных и обнуляющих дуг. Разработанный алгоритм реализован в виде программного инструмента с открытым исходным кодом, которые регистрирует наблюдаемое поведение расширенной сети Петри в журнале событий.

Приоритеты срабатывания переходов являются одним из способов управления поведением сетей Петри для обеспечения их живости и ограниченности. Необходимость в них обусловлена ограниченностью ресурсов, характеризующей большинство реальных информационных систем. Реализован предложенный ранее алгоритм вычисления приоритетов срабатывания переходов в сетях Петри. Проведены эксперименты по вычислению приоритетов в моделях сложных распределенных вычислений.

Выявлены типичные паттерны асинхронного взаимодействия агентов в сложных мультиагентных системах. Построены формальные модели паттернов в виде композиции сетей Петри, а также изучены их семантические свойства. Показано, как паттерны асинхронного взаимодействия агентов могут применяться для синтеза структурированных моделей мультиагентных систем по журналам событий.

Предложен новый метод проверки соответствия между моделями информационных систем и примерами их наблюдаемого поведения из журналов событий, когда допускается не только полное, но и частичное соответствие последовательностей наблюдаемого и моделируемого поведения. В рамках метода предложена специальная метрика оценки соответствия. Установлено, что предложенный метод удовлетворяет свойству монотонности, т. е. с ростом частичного соответствия последовательностей наблюдаемого и моделируемого поведения возрастает значение метрики оценки соответствия.

В процессе эксплуатации информационной системы организация ее процессов может изменяться. Исследована задача выявления фрагментов BPMN-модели, которые по-прежнему соответствуют наблюдаемому поведению, представленному в журналах событий. Предложенный метод основан на выявлении и анализе зависимостей между событиями процесса.

Усовершенствован разработанный ранее метод декомпозиции моделей в нотации сетей Петри, который используется для исправления фрагментов модели в соответствии с журналами событий. Разработанный метод основан на построении графа декомпозиции, представляющего максимальное разбиение модели процесса, и минимального остовного дерева, включающего все фрагменты модели, которые необходимо исправить.

Исследована задача построения формальной модели для реальной системы биржевой торговли по ее описанию. Разработана модель в формализме высокоуровневых сетей Петри, которая описывает поведение компонентов системы биржевой торговли с точки зрения того, как обрабатываются заказы на покупку и продажу ценных бумаг на бирже. Реализован прототип программного инструмента, который регистрирует исполнение модели системы биржевой торговли в виде динамики изменений в книге заказов.

Разработан метод анализа первичных данных, получаемых из систем биржевой торговли. Метод преобразует журналы событий в формат, который допускает их автоматизированную обработку для дальнейшего синтеза формальных моделей систем биржевой торговли.

Предложен оригинальный метод мониторинга процесса ведения уголовных дел с целью выявления аномалий, которые не допускаются принятыми регламентами. Данный метод основан на анализе журналов событий. Разработана формальная модель процесса ведения уголовных дел, которая учитывает предъявляемые требования. С помощью анализа журналов событий показано, как выявить аномалии, связанные с несоблюдением временных ограничений и зацикливанием.

Разработан новый метод представления журналов событий в виде автономных реляционных баз данных (БД) на основе встраиваемой СУБД SQLite. Такие журналы событий названы SQLite-EventLogs. Метод реализован в виде компонента библиотеки LDOPA и апробирован на наборе искусственных и реальных журналов событий. Сравнительные эксперименты по эффективности представления журналов событий в виде SQLite-EventLogs показали большую эффективность по сравнению с классическим представлением журналов событий.

Проведено исследование и выполнена разработка модификации структуры данных «B-дерево» – B*+- деревья. Они используется для индексирования таблиц реляционных баз данных. Разработано расширение, реализующее индексирование с помощью B*+-дерева, для реляционной встраиваемой СУБД SQLite. Преимущество разработанной структуры данных заключается в оптимизации работы с журналами событий в формате SQLite-EventLog.

Разработан новый метод автоматического конструирования UML диаграмм деятельности по журналам событий. Метод основан на параметрической схеме синтеза, которая включает три этапа последовательной трансформации модели – от журнала событий до диаграммы деятельности.

Степень внедрения, рекомендации по внедрению или итоги внедрения результатов НИР

Предложенные теоретические методы анализа и верификации автоматных моделей информационных систем ориентированы на возможность их практической реализации. Разработанные методы синтеза, исправления и проверки соответствия прошли апробацию на журналах событий реальных информационных систем.

Дополнительные результаты

5 апреля 2019 год научный сотрудник лаборатории ПОИС А.А. Мицюк успешно защитил диссертацию “Structure-Preserving Process Model Repair Based on Event Logs” на соискание ученой степени кандидата компьютерных наук НИУ ВШЭ в диссертационном совете по компьютерным наукам НИУ ВШЭ (научный руководитель: заведующая лабораторией ПОИС И.А. Ломазова).

Статья “Monotone Conformance Checking for Partially Matching Designed and Observed Processes” ведущего научного сотрудника лаборатории ПОИС А.А. Каленковой в соавторстве с Полывяным А.А. (Университет Мельбурна, Австралия) была признана лучшей статьей, представленной на международной конференции “International Conference on Process Mining (ICPM 2019)”, которая проходила 24-26 июня 2019 года в г. Аахен (Германия).

Статья “A Method to Improve Workflow Net Decomposition for Process Model Repair” научного сотрудника лаборатории ПОИС А.А. Мицюка в соавторстве со стажером-исследователем С.Е. Тихоновым была признана лучшей статьей, представленной на международной конференции “Analysis of Images, Social Networks and Texts (AIST 2019)”, которая проходила 17-19 июля 2019 года в г. Казань (Россия).

Публикации по проекту:


Каленкова А. А., Колесников Д. А. Применение генетического алгоритма для нахождения редакционного расстояния между моделями процессов // Моделирование и анализ информационных систем. 2018. Т. 25. № 6. C. 711-725. doi
Gnatenko A., Zakharov V. On the Expressive Power of Some Extensions of Linear Temporal Logic // Автоматика и вычислительная техника. 2019. Vol. 53. No. 7. P. 663-675. doi
Zakharov V., Abbas M. M. Even Simple Processes of Pi-calculus are Hard for Analysis // Automatic Control and Computer Sciences, USA. 2019. Vol. 53. No. 7. P. 589-606. doi
N. S. Zubkova, S. A. Shershakov Method for Building UML Activity Diagrams from Event Logs // Труды Института системного программирования РАН. 2019. Vol. 31. No. 4. P. 139-150. doi
Kalenkova A. A., Burattin A., de L. M., van d. A. W., Sperduti A. Discovering high-level BPMN process models from event data // Business Process Management Journal. 2019. Vol. 25. No. 5. P. 995-1019. doi
Pavel P., Mitsyuk A. A. Simulating Petri Nets with Inhibitor and Reset Arcs // Труды Института системного программирования РАН. 2019. Vol. 31. No. 4. P. 151-162. doi
A.M. Rigin, S.A. Shershakov SQLite RDBMS Extension for Data Indexing Using B-tree Modifications // Труды Института системного программирования РАН. 2019. Vol. 31. No. 3. P. 203-216. doi
K.G. Serebrennikov Computing Transition Priorities for Live Petri Nets // Труды Института системного программирования РАН. 2019. Vol. 31. No. 4. P. 163-174. doi
Kirill A., Irina L. What Has Remained Unchanged in Your Business Process Model?, in: 21st IEEE Conference on Business Informatics (CBI).: IEEE Computer Society, 2019. С. 551-558. 
Захаров Владимир Анатольевич, Гнатенко Антон Романович Верификация моделей реагирующих систем относительно одного расширения темпоральной логики CTL*, in: Материалы XIII Международного семинара "Дискретная математика и ее приложения" имени академика О.Б. Лупанова (Москва, МГУ, 17-22 июня 2019). Москва : Изд-во механико-математического факультета МГУ, 2019. С. 263-266. 
Захаров В. А., Винарский Е. М. О задаче верификации для одного класса автоматов реального времени, in: Материалы XIII Международного семинара "Дискретная математика и ее приложения" имени академика О.Б. Лупанова (Москва, МГУ, 17-22 июня 2019). Москва : Изд-во механико-математического факультета МГУ, 2019. С. 257-260. 
Захаров В. А., Жайлауова Ш. Р. О проблеме эквивалентности недетерминированных автоматов-преобразователей над однобуквенным выходным алфавитом, in: Материалы XIII Международного семинара "Дискретная математика и ее приложения" имени академика О.Б. Лупанова (Москва, МГУ, 17-22 июня 2019). Москва : Изд-во механико-математического факультета МГУ, 2019. С. 272-274. 
Carrasquel G. J. C., Lomazova I. A., Itkin I. L. Towards a Formal Modelling of Order-driven Trading Systems using Petri Nets: A Multi-Agent Approach, in: Proceedings of the MACSPro Workshop 2019.: CEUR-WS.org, 2019. С. 92-103. 
Alexandra K., Irina L. Detection of Anomalies in the Criminal Proceedings Based on the Analysis of Event Logs, in: Analysis of Images, Social Networks and Texts. 8th International Conference, AIST 2019, Lecture Notes in Computer Science, Revised Selected Papers. Cham : Springer, 2019. С. 401-410. 
Материалы XIII Международного семинара «Дискретнаяматематика и ее приложения», имени академика О.Б. Лупанова (Москва, МГУ, 17–22 июня 2019 г.). Москва : Изд-во механико-математического факультета МГУ, 2019. 
Roman A. N., Irina A. L. Asynchronous Interaction Patterns for Mining Multi-Agent System Models from Event Logs, in: Proceedings of the MACSPro Workshop 2019.: CEUR-WS.org, 2019. С. 62-73. 
Skobtsov A., Kalenkova A. A. Efficient Comparison of Process Models using Tabu Search Algorithm, in: Proceedings of the MACSPro Workshop 2019.: CEUR-WS.org, 2019. 
Skobtsov A., Kalenkova A. A. Using Heuristic Algorithms for Fast Alignment between Business Processes and Goals, in: 2019 IEEE 23rd International Enterprise Distributed Object Computing Workshop (EDOCW).: IEEE, 2019. С. 85-91. 
Semyon E. T., Mitsyuk A. A. A Method to Improve Workflow Net Decomposition for Process Model Repair, in: Analysis of Images, Social Networks and Texts. 8th International Conference AIST 2019.: Springer, 2019. С. 411-423. 
Polyvyanyy A., Kalenkova A. A. Monotone Conformance Checking for Partially Matching Designed and Observed Processes, in: 2019 International Conference on Process Mining (ICPM).: IEEE, 2019. С. 81-88. 
Sergey A. S. Multi-Perspective Process Mining with Embedding Configurations into DB-based Event Logs, in: Proceedings of the International Conference on Software Testing, Machine Learning and Complex Process Analysis (TMPA-2019).: Springer, 2020.