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.