• A
  • A
  • A
  • АБВ
  • АБВ
  • АБВ
  • А
  • А
  • А
  • А
  • А
Обычная версия сайта

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

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

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

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

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

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

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

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

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

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

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

Исследованы два фрагмента языка LP-CTL*, позволяющие задавать спецификации модели Крипке. Построены алгоритмы верификации моделей Крипке относительно этих спецификаций.

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

Доказано существование полиномиального алгоритма проверки эквивалентности детерминированных 2-ленточных автоматов.

Исследована co-NP-полнота задачи проверки свойств информационной безопасности моделей нерекурсивных криптографических протоколов.

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

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

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

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

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

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

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

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

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

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

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

В 2018 году под руководством заведующей лаборатории ПОИС Ломазовой И.А. были защищены 2 PhD диссертации по тематике работы лаборатории:

- 5 июня 2018 года с.н.с. лаборатории ПОИС Каленкова А.А. защитила диссертацию ”Learning high-level models from event data” в Техническом Университете Эйндховена;

- 10 октября 2018 года н.с. лаборатории ПОИС Дворянский Л.В. защитил диссертацию ”Nested Petri Nets: behaviour analysis and time semantics” в Берлинском университете имени Гумбольта.

В 2018 году студенческая работа Давыдовой К.В. «Метод построения гибридных UML моделей по журналам событий систем с сервис-ориентированной архитектурой», выполненная под руководством н.с. лаборатории ПОИС Шершакова С.А. заняла третье место на конкурсе НИРС в номинации «Лучшая научно-исследовательская работа по компьютерным наукам для студентов магистратуры и выпускников 2017 года».

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


Proceedings of 9th Workshop “Program Semantics, Specification and Verification: Theory and Applications" (PSSV-2018), Yaroslavl, Russia, June 21-22, 2018 / Ed. by V. Zakharov, Н. В. Шилов. Yaroslavl : Ярославский государственный университет им. П.Г. Демидова, 2018.
Zakharov V., Gnatenko A. R. On the expressive power of some extensions of Linear Temporal Logic, in: Proceedings of 9th Workshop “Program Semantics, Specification and Verification: Theory and Applications" (PSSV-2018), Yaroslavl, Russia, June 21-22, 2018 / Ed. by V. Zakharov, Н. В. Шилов. Yaroslavl : Ярославский государственный университет им. П.Г. Демидова, 2018. P. 29-36 .
Захаров В. А., Аббас М. М. Даже простые процессы pi-исчисления трудны для анализа // Моделирование и анализ информационных систем. 2018. Т. 25. № 6. С. 589-606. doi
Shunin T., Zubkova N., Sergey Shershakov. Neural Approach to the Discovery Problem in Process Mining, in: Analysis of Images, Social Networks and Texts. 7th International Conference AIST 2018 / Ed. by W. van der Aalst, D. I. Ignatov. Springer, 2018. P. 261-273. doi
Tarantsova P. D., Kalenkova A. A. Constructing Regular Expressions from Real-life Event Logs, in: Analysis of Images, Social Networks and Texts. 7th International Conference AIST 2018 / Ed. by W. van der Aalst, D. I. Ignatov. Springer, 2018. P. 274-280.
Gnatenko A. R., Zakharov V. On the Model Checking of Finite State Transducers over Semigroups // Proceedings of the Institute for System Programming of the RAS. 2018. Vol. 30. No. 3. P. 303-324. doi
Захаров В. А., Гнатенко А. Р. О выразительных возможностях некоторых расширений линейной темпоральной логики // Моделирование и анализ информационных систем. 2018. Т. 25. № 5. С. 506-524. doi
Захаров В. А. Полиномиальный алгоритм проверки эквивалентности детерминированных двухленточных автоматов // В кн.: Дискретные модели в теории управляющих систем: Х Международная конференция, Москва и Подмосковье, 23-25 мая 2018 г. : Труды / Под общ. ред.: Д. С. Романов. МГУ, МАКС Пресс, 2018. С. 128-130.
Гнатенко А. Р., Захаров В. А. Языки спецификаций моделей Крипке на основе темпоральных логик и их выразительные возможности // В кн.: Дискретные модели в теории управляющих систем: Х Международная конференция, Москва и Подмосковье, 23-25 мая 2018 г. : Труды / Под общ. ред.: Д. С. Романов. МГУ, МАКС Пресс, 2018. С. 131-133.
Roman A. Nesterov, Irina A. Lomazova. Compositional Process Model Synthesis based on Interface Patterns, in: Tools and Methods of Program Analysis: 4th International Conference, TMPA 2017, Moscow, Russia, March 3-4, 2017, Revised Selected Papers Vol. 779: Communications in Computer and Information Science. Cham: Springer, 2018. doi P. 151-162. doi
Bernardinello L., Irina Lomazova, Roman Nesterov, Pomello L. Compositional Discovery of Workflow Nets from Event Logs Using Morphisms, in: Proceedings of the International Workshop on Algorithms & Theories for the Analysis of Event Data 2018 Vol. 2115: CEUR Workshop Proceedings. CEUR-WS.org, 2018. P. 23-38.
Nesterov R.A., Mitsyuk A.A., Lomazova I.A. Simulating Behavior of Multi-Agent Systems with Acyclic Interactions of Agents // Proceedings of the Institute for System Programming of the RAS. 2018. Vol. 30. No. 3. P. 285-302. doi
Дискретные модели в теории управляющих систем: Х Международная конференция, Москва и Подмосковье, 23-25 мая 2018 г. : Труды / Под общ. ред.: Д. С. Романов. МГУ, МАКС Пресс, 2018.
Захаров В. А., Гнатенко А. Р. Языки спецификаций моделей Крипке на основе темпоральных логик и их выразительные возможности С. 131-133.
Kalenkova A. A., Агеев А. А., Lomazova I. A., van der Aalst W. E-Government Services: Comparing Real and Expected User Behavior, in: BPM 2017 International Workshops, Barcelona, Spain, September 10-11, 2017, Revised Papers Vol. 308. Springer, 2018. P. 484-496. doi
Mitsyuk A. A., Котылев Я. В. Layered Layouts for Software Systems Visualization Using Nested Petri Nets, in: Tools and Methods of Program Analysis: 4th International Conference, TMPA 2017, Moscow, Russia, March 3-4, 2017, Revised Selected Papers Vol. 779: Communications in Computer and Information Science. Cham: Springer, 2018. doi Ch. 11. P. 127-138. doi
Mitsyuk A. A. Non-Local Correction of Process Models Using Event Logs, in: Proceedings of the 2017 Ivannikov ISPRAS Open Conference. Los Alamitos : IEEE Computer Society, 2018. Ch. 2. P. 6-11. doi