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

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

Приоритетные направления развития: инженерные науки
2016

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

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

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

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

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

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

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

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

Дано определение инварианта позиций для вложенной сети Петри. Разработан алгоритм нахождения инвариантов позиций вложенных сетей Петри.

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

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

В области извлечения и анализа процессов были получены следующие результаты:

Разработан новый метод синтеза систем переходов по журналам событий информационных систем. Этот метод позволяет балансировать между точностью (способностью проигрывать только трассы из журнала событий) и компактностью системы переходов: для более часто встречающихся участков трасс строится наиболее точная система переходов, в том время как для редко встречающихся последовательностей событий строится компактная модель, допускающая дополнительное поведение. Этот метод был реализован в виде компонента системы ProM (Process mining framework).

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

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

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

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

 

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


Dworzanski L. W. Consistent Timed Semantics for Nested Petri Nets with Restricted Urgency, in: Formal Modeling and Analysis of Timed Systems Vol. 9884. Switzerland : Springer, 2016. doi Ch. 1. P. 3-18. doi
Dworzanski L. W., Lomazova I. A. Structural Place Invariants for Analyzing the Behavioral Properties of Nested Petri Nets, in: Application and Theory of Petri Nets and Concurrency. 37th International Conference, PETRI NETS 2016, Toruń, Poland, June 19-24, 2016. Proceedings Vol. 9698: Lecture Notes in Computer Science. Switzerland : Springer, 2016. doi P. 325-344. doi
Zakharov V., Temerbekova G. On the minimization and equivalence checking of sequential reactive systems // Системная информатика. 2016. No. 7. P. 33-44.
Vladislav Podymov. An Efficient Equivalence-checking Algorithm for a Model of Programs with Commutative and Absorptive Statements // Fundamenta Informaticae. 2016. Vol. 147. No. 2-3. P. 315-336.
Davydova K. V., Shershakov S. A. Mining Hierarchical UML Sequence Diagrams from Event Logs of SOA Systems while Balancing between Abstracted and Detailed Models // Proceedings of the Institute for System Programming of the RAS. 2016. Vol. 28. No. 3. P. 85-102. doi
Lomazova I. A., Popova-Zeugmann L. Controlling Petri Net Behavior using Priorities for Transitions // Fundamenta Informaticae. 2016. Vol. 143. No. 1-2. P. 101-112. doi
Захаров В. А., Козлова Д. Г. Темпоральная логика для верификации автоматов-преобразователей // В кн.: Материалы XII Международного семинара "Дискретная математика и её приложения" имени академика О.Б. Лупанова (Москва, МГУ, 20-25 июня 2016г.) / Под общ. ред.: О. М. Касим-Заде. М. : Изд-во механико-математического факультета МГУ, 2016. С. 204-206.
Захаров В. А., Джусупекова З. А. О проверке k-значности конечных автоматов-преобразователей над полугруппами // В кн.: Материалы XII Международного семинара "Дискретная математика и её приложения" имени академика О.Б. Лупанова (Москва, МГУ, 20-25 июня 2016г.) / Под общ. ред.: О. М. Касим-Заде. М. : Изд-во механико-математического факультета МГУ, 2016. С. 190-192.
Shugurov I., Mitsyuk A. A. Applying MapReduce to Conformance Checking // Proceedings of the Institute for System Programming of the RAS. 2016. Vol. 28. No. 3. P. 103-122. doi
Захаров В. А., Темербекова Г. Г. Оптимизирующие преобразования потоковых программ // В кн.: Материалы XII Международного семинара "Дискретная математика и её приложения" имени академика О.Б. Лупанова (Москва, МГУ, 20-25 июня 2016г.) / Под общ. ред.: О. М. Касим-Заде. М. : Изд-во механико-математического факультета МГУ, 2016. С. 232-234.
Sergey A. Shershakov, Anna A. Kalenkova, Lomazova I. A. Transition Systems Reduction: Balancing between Precision and Simplicity, in: International Workshop on Algorithms and Theories for the Analysis of Event Data, ATAED 2016; Torun; Poland; 20-21 June 2016 / Ed. by W. van der Aalst, R. Bergenthum, J. Carmona. Vol. 1592. Torun : CEUR Workshop Proceedings, 2016. P. 78-95.
Zakharov V., Kozlova D. On the model checking of sequential reactive systems, in: Proceedings of the 25th International Workshop on Concurrency, Specification and Programming, Rostock, Germany, September 28-30, 2016. Vol. 1698. Humboldt-Universität zu Berlin, 2016. P. 233-244.
Mitsyuk A. A., Shugurov I. On Process Model Synthesis Based on Event Logs with Noise / Пер. с рус. // Automatic Control and Computer Sciences. 2016. Vol. 50. No. 7. P. 460-470. doi
Захаров В. А., Темербекова Г. Г. О минимизации конечных автоматов-преобразователей над полугруппами // Моделирование и анализ информационных систем. 2016. Т. 23. № 6. С. 741-753.
Kalenkova A. A., van der Aalst W., Lomazova I. A., Rubin V. Process mining using BPMN: relating event logs and process models, in: MODELS '16 Proceedings of the ACM/IEEE 19th International Conference on Model Driven Engineering Languages and Systems. NY : ACM, 2016. P. 123-123. doi
Samokhvalov D., Dworzanski L. W. Automatic Code Generation from Nested Petri nets to Event-based Systems on the Telegram Platform // Proceedings of the Institute for System Programming of the RAS. 2016. Vol. 28. No. 3. P. 65-84. doi
Lomazova I. A., Ermakova V. Verification of Nested Petri Nets Using an Unfolding Approach, in: CEUR Workshop Proceedings Vol. 1591: Petri Nets and Software Engineering. International Workshop, PNSE'16, Torun, Poland, June 20-21, 2016. Proceedings. CEUR Workshop Proceedings, 2016. P. 93-112.
Shershakov S. DPMine graphical language for automation of experiments in process mining / Пер. с рус. // Automatic Control and Computer Sciences. 2016. Vol. 50. No. 7. P. 477-485. doi
Dworzanski L. W., Lomazova I. A. Automatic construction of systems of distributed components from nested Petri nets models / Пер. с рус. // Programming and Computer Software. 2016. Vol. 42. No. 5. P. 292-306. doi