• A
  • A
  • A
  • ABC
  • ABC
  • ABC
  • А
  • А
  • А
  • А
  • А
Regular version of the site

Modeling and analysis of the behavior of distributed process-aware information systems

Priority areas of development: engineering science
2016
The project has been carried out as part of the HSE Program of Fundamental Studies.

Goal of research: The goal of the research is to develop new approaches for modeling, analysis, verification of sequential programs and distributed information systems.

Methodology: Discrete mathematics, automata theory, mathematical logic, methods of formal program verification, and algebra were used for the development of new approaches for modeling and analysis of sequential programs. Discrete mathematics, theory of Petri nets, automata theory, and Process mining techniques were used for the development of new approaches for the analysis of distributed information systems behavior.

Empirical base of research: The empirical base of the research is represented by sequential programs, distributed software systems, and event logs, containing history of the software system’s work.

Results of research:

In the field of analysis of program’s and distributed information system’s behavior, we obtained the following results:

An algorithm for the minimization of finite-state transducers, modeling the behavior of sequential programs, was developed. A formal specification language and a verification algorithm based on the use of this language were developed for the analysis of finite-state transducers. The proposed algorithms were justified.

A polynomial time algorithm for checking the equivalence of two sequential programs was developed. This algorithm is based on algebraic statements and can be applied to propositional programs (final-state machines with states corresponding to program instructions).

A novel formalism for modeling multi-agent systems with time using nested Petri nets with temporal arcs was proposed. The semantics of these nets is based on the semantics of Petri nets with time arcs and restricted urgency.

A definition of place invariants for nested Petri nets was proposed. An algorithm for finding place invariants for nested Petri nets was developed as well.

An algorithm for finding unfoldings of safe conservative nested Petri nets was proposed. It was shown that any safe conservative nested Petri net can be transformed into a classical Petri net so that their reachability graphs are isomorphic.

An approach for the generation of code for multi-agent systems from nested Petri nets was proposed. A language (called Action Language), describing the logic of interactions between agents, was developed. A compiler for Action Language and a program assembling sub-programs attached to the Petri net transitions were implemented. It was demonstrated that the code generated can be used for conducting search-and-rescue operations in earthquakes.

In the field of Process mining the following results were obtained:

A novel method for the synthesis of transition systems from the event logs of information systems was proposed. This method allows balancing between precision (an ability to replay event log traces only) and simplicity (compactness) of the transition systems: for the frequent process behavior precise transition systems are constructed, while for the rare sequences of events more compact and less precise models are discovered. This method was implemented as a component of the ProM (Process mining framework) system.

A method for the synthesis of hierarchical UML sequence diagrams from the event logs of service-oriented information systems was developed and implemented. This method allows finding the balance between low-level and high-level process diagrams.

A distributed method for checking conformance of an event log and a process model was designed and implemented. This method was tested on large real-life event logs of information systems. As a result of the experiments the most suitable tools for distributed conformance checking were selected.

Level of implementation,  recommendations on implementation or outcomes of the implementation of the results

All the proposed theoretical methods are focused primarily on the possibility of their practical application. Methods for the analysis of nested Petri nets and Process mining methods were implemented and tested on various input data, for instance, Process mining techniques were tested on real event logs of information systems. This leads us to believe that the presented techniques are suitable for solving practical problems.

Publications:


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