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

Новые методы решения задач извлечения и анализа процессов и их применение для проектирования информационных систем

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

Цель работы

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

16 сентября 2020 года научных сотрудник лаборатории ПОИС С.А. Шершаков успешно защитил диссертацию «Методы и инструменты повышения эффективности алгоритма майнинга процессов» на соискание ученой степени кандидата компьютерных наук НИУ ВШЭ в диссертационном совете по компьютерным наукам НИУ ВШЭ (научный руководитель заведующая лабораторией ПОИС И.А. Ломазова).

Статья «Checking Conformance between Colored Petri Nets and Event Logs» стажера-исследователя лаборатории ПОИС Х.С. Карраскеля Гамеса, заведующей лабораторией ПОИС И.А. Ломазовой в соавторстве с Х. Мешерау (Абдельхамид Мехриский университет Константина 2, Алжир) была признана одной из лучших статей, представленных на международной конференции «Analysis of Images, Social Networks and Texts (AIST-2020)», которая проходила 15-16 октября 2020 года.

При организационной поддержке НУЛ ПОИС 3-4 ноября 2020 года прошел международный семинар «Program Semantics, Specification and Verification (PSSV2020)». Сотрудники НУЛ ПОИС также приняли участие в организации трека «Process mining» в рамках международной конференции «Analysis of Images, Social Networks and Texts (AIST-2020) и международной конференции «Modeling and Analysis of Complex Systems and Processes (MACSPro-2020)», проходившей 22-24 октября 2020 года.

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


Gnatenko A., Zakharov V. Using an extension of CTL* for specification and verification of sequential reactive systems // Системная информатика. 2020. Vol. 17. P. 21-32. 
Захаров В. А. Эффективные алгоритмы проверки эквивалентности для некоторых классов автоматов // Моделирование и анализ информационных систем. 2020. Т. 27. № 3. C. 260-303. doi
Шершаков С. А. “VTMine for Visio”: инструмент графического моделирования в области Process Mining // Моделирование и анализ информационных систем. 2020. Т. 27. № 2. C. 194-217. doi
Mecheraoui K., Carrasquel G. J. C., Lomazova I. A. Compositional conformance checking of nested petri nets and event logs of multi-agent systems, in: Proceedings of the Conference on Modeling and Analysis of Complex Systems and Processes 2020 (MACSPro 2020).: CEUR Workshop Proceedings, 2020. С. 34-45. 
Carrasquel G. J. C., Lomazova I. A., Rivkin A. Modeling Trading Systems using Petri Net Extensions, in: Proceedings of the International Workshop on Petri Nets and Software Engineering co-located with 41st International Conference on Application and Theory of Petri Nets and Concurrency (PETRI NETS 2020).: CEUR-WS.org, 2020. С. 118-137. 
Yaroslav V. K., Mitsyuk A. A. Software System Behavior Can Be Analyzed with Visual Analytics, in: Proceedings of the Conference on Modeling and Analysis of Complex Systems and Processes 2020 (MACSPro 2020).: CEUR Workshop Proceedings, 2020. С. 46-56. 
Bernardinello L., Lomazova I. A., Nesterov R., Pomello L. Property-Preserving Transformations of Elementary Net Systems Based on Morphisms, in: Proceedings of the International Workshop on Petri Nets and Software Engineering co-located with 41st International Conference on Application and Theory of Petri Nets and Concurrency (PETRI NETS 2020).: CEUR-WS.org, 2020. С. 49-67. 
Mecheraoui K., Carrasquel G. J. C., Lomazova I. A. Compositional Conformance Checking of Nested Petri Nets and Event Logs of Multi-Agent Systems / Cornell University. Series Computer Science "arxiv.org". 2020.