The main thrust of the laboratory research activity is helping to provide a formal framework for understanding, designing, analyzing and implementing complex distributed and real-time (timed, stochastic, hybrid) systems (D&RTS) such as communication protocols, process control systems, production and management systems, etc. These systems are becoming increasingly clear to be notoriously difficult to comprehend and, hence, to design and analyze. Therefore there is an obvious need for thorough modeling the systems at all stages of their design to use formal methods that should be `designer-friendly', mathematically precise and able to expose sufficient details about the system behavior. This formal framework should lead to methodologies for providing the systems correct and more generally for deriving their properties. The ultimate goal can be reached by using and extending the achievements of concurrency theory. The investigation undertaken in the laboratory is divided into the following workpackages and tasks:
- The definition, analysis, comparison and unification of formal models and behavioral equivalences for D&RTS, in order to get better understanding the inherent concurrent, nondeterministic and timing nature of the system behavior and to strengthen the existing and derive new results based on the relationships between the individual models. The main goal here is the category-theoretic unification of timed models and behavioral equivalences, the investigation of interrelations of stochastic equivalences for fluid stochastic Petri nets, the construction of new algorithms for simulation and bisimulation of dynamical and hybrid systems, based on invariants and constraints.
- The research and development of real-time process calculi to allow one to compositionally construct and prove the correctness of the behavior of D&RTS and the selection among behavioral equivalences a few candidate congruences which are proper to be transported to a real-time process algebra framework, in order to provide more abstract representations of the systems. In particular, we carry out research in developing and investigating operational and denotational semantics of discrete stochastic Petri box calculi and their stochastic equivalences.
- The elaboration and evolution of logic-based specification and verification methods for qualitative and quantitative reasoning about the behavior of D&RTS. The intention within the topic is to develop algorithms for parametric timing behavior analysis of concurrent and real time systems represented by different classes of time Petri nets, w.r.t. real-time temporal logics formulas.
- Tools design and case studies, in order to implement, compare and evaluate the theoretical methods to be proposed and show applicability and flexibility of the methods. More concretely, we design a software tool that incorporate several verification methods, including real time model checking and equivalence checking, for different classes of Petri nets with time characteristics and time parameters.