Vergleichende Analyse und Verifikation für Verteilte Sicherheitskritische Systeme (CAVER)
Zusammenfassung der Projektergebnisse
The increasing size and the networked and real-time nature of telecommunications, automatic controllers, web services, mobile and embedded devices, etc. confront us with the problem of the precise comprehension of their behavior and, hence, of the assurance of their correct functioning. The general approaches to cope with the problem are founded on rigorous formalisms and computer aided tools which can be helpful in the thorough modeling of the systems at all stages of their design and implementation. The project CAVER brought new and efficient theoretical frameworks and software instruments that are mathematically precise, “designer-amicable”, and able to expose sufficient details about the systems’ structures and behaviors, and thus join the existing effort of many other teams in the theory of concurrent and real-time systems. In the context of event- and relation-oriented models, some uniform generalizations of classical “concurrency axioms” were introduced, their power, limitations and interrelations were studied, and alternative characterizations in the terms of algebraic properties of ortomodular lattices were provided. Using category-theoretic methods, the existence of a chain of coreflections, leading from the category of transition systems with independence to a category of specially designed models of marked Scott domains, has been shown; interrelations between syntactic and semantic categories of timed/untimed causality-based models were established; category-theoretic and logic equivalents for timed history preserving bisimulation have been obtained in the context of categories of timed causal trees. Several methods for constructing configuration-based and residual-based transition systems from various classes of event-oriented models were developed, isomorphism results between the transition systems have been obtained in a full spectrum of semantics (interleaving, step, pomset, multiset). The question of characterization of Petri net synthesizable state spaces was investigated under various restrictions: limited number of transitions, constrained shapes of reachability graphs, special target classes of Petri nets. A range of necessary and sufficient conditions for synthesizability have been obtained. The conditions give rise to a number of specialised synthesis algorithms which demonstrate a better runtime in comparison to the general synthesis algorithm. The conditions are applicable for a pre-synthesis quick-failure procedure which allows rejecting non-synthesizable inputs without initiating the synthesis itself. The "true-concurrent" and non-deterministic semantics in terms of branching processes of timed Petri nets (TdPNs) with an infinite number of transitions and places with unlimited number of tokens, and semantics of (maximal) step of concurrent transitions has determined. It has been proved that unfolding – the maximal branching process – is the greatest element of the complete lattice, built on branching processes of TdPNs with step semantics. It has been shown that this result is true in the case of the maximal step semantics, only if some restrictions on TdPNs are imposed and a new class of branching processes and unfoldings is defined. In the context of time safe Petri nets and their subclasses, the interrelations between various trace and (back-forth)-bisimulation equivalences in different (interleaving, step, causal/occurrence nets) semantics have been established, and a hierarchy of the equivalent nets has been constructed. The structure and behavior of dense-time safe Petri nets with dynamic priorities (DPTPNs) have been defined and investigated, an algorithm for constructing a finite abstraction of the behavior of DPTPNs in the form of zone graph hase been developed and evaluated. The abstraction allows for DPTPN verification based on real-time temporal logic TCTL. A novel approach for checking satisfiability of non-linear constraints over the reals has been proposed. It is based on conflict resolution in a CDCL-style calculus, using a composition of symbolical and numerical methods. The approach covers a large number of computable non-linear real functions such as polynomials, rational or trigonometrical functions and beyond. A prototypical implementation has been compared with state-of-the-art SMT solvers.
Projektbezogene Publikationen (Auswahl)
- "Truly concurrent" and nondeterministic semantics of discrete-time Petri nets. Programming and Computer Software Vol. 42(4), Springer (2016) 187-197
Virbitskaite, I. B., Borovlev, V. A., Popova-Zeugmann, L.
(Siehe online unter https://doi.org/10.1134/S0361768816040071) - Branching Processes of Timed Petri Nets. In: Proc. 10th Int. Conf. PSI’15, Kazan, August 2015. Lecture Notes in Computer Science Vol. 9609, Springer (2016) 303-313
Virbitskaite I., Borovlyov V., Popova-Zeugmann L.
(Siehe online unter https://doi.org/10.1007/978-3-319-41579-6_23) - Characterising Petri Net Solvable Binary Words. In: Proc. PETRI NETS 2018: 37th International Conference on Applications and Theory of Petri Nets and Concurrency. Lecture Notes in Computer Science Vol. 9698, Springer (2016) 39-58
Best, E., Erofeev, E., Schlachter, U., Wimmel, H.
(Siehe online unter https://doi.org/10.1007/978-3-319-39086-4_4) - Conditions for Petri Net Solvable Binary Words. Transactions on Petri Nets and Other Models of Concurrency Vol. 11 (2016) 137-159
Barylska, K., Best, E., Erofeev, E., Mikulski, L., Piatkowski, M.
(Siehe online unter https://doi.org/10.1007/978-3-662-53401-4_7) - Towards using exact real arithmetic for initial value problems. Lecture Notes in Computer Science v. 9609, 2016, pages 61-74 . Springer
Brauße F., Korovina M., and Müller N.
(Siehe online unter https://doi.org/10.1007/978-3-319-41579-6_6) - True Concurrent Equivalences in Time Petri Nets. Fundamenta Informaticae Vol 149(4), IOS Press (2016) 401-418
Virbitskaite, I., Bushin, D., Best, E.
(Siehe online unter https://doi.org/10.3233/FI-2016-1454) - Using Taylor Models in Exact Real Arithmetic. Lecture Notes in Computer Science v. 9582, 2016, pages 474-488. Springer
Brauße F., Korovina M., and Müller N.
(Siehe online unter https://doi.org/10.1007/978-3-319-32859-1_41) - Configuration- and Residual-Based Transition Systems for Event Structures with Asymmetric Conflict. In: Proc. SOFSEM 2017: Theory and Practice of Computer Science. Lecture Notes in Computer Science Vol. 10139 Springer (2017) 132-146
Best E., Gribovskaya N., Virbitskaite I.
(Siehe online unter https://doi.org/10.1007/978-3-319-51963-0_11) - Equivalence and lumpability of FSPNs. (ASMTA'17), Lecture Notes in Computer Science 10378, 2017, pages 16-31. Springer
Bause F., Buchholz P., Tarasyuk I.V., Telek M.
(Siehe online unter https://doi.org/10.1007/978-3-319-61428-1_2) - Equivalences for fluid stochastic Petri nets. Siberian Electronic Mathematical Reports 14, 2017, pages 317-366
Tarasyuk I.V., Buchholz P.
(Siehe online unter https://doi.org/10.17377/semi.2017.14.029) - Complexity for partial computable functions over computable Polish spaces, Mathematical Structures in Computer Science 28(3), 2018, 429-447
Korovina M., Kudinov O.
(Siehe online unter https://doi.org/10.1017/S0960129516000438) - From Event-Oriented Models to Transition Systems. In: Proc. PETRI NETS 2018: 39th International Conference on Applications and Theory of Petri Nets and Concurrency. Lecture Notes in Computer Science Vol. 10877, Springer (2018) 117-139
Best, E., Gribovskaya, N., Virbitskaite, I.
(Siehe online unter https://doi.org/10.1007/978-3-319-91268-4_7) - Stochastic equivalence for performance analysis of concurrent systems in dtsiPBC. Siberian Electronic Mathematical Reports 15, 2018, pp 1743-1812
Tarasyuk I.V., Macia S.H., Valero R.V.
(Siehe online unter https://doi.org/10.33048/semi.2018.15.144) - Continuous Constraint Solving in CDCL-style. FROCOS 2019, Lecture Notes in Computer Science v. 11715 , pages 131–148, 2019. Springer
Brauße F., Korovin K., Korovina M., Müller N. Th.
(Siehe online unter https://doi.org/10.1007/978-3-030-29007-8_8) - Logical characterization of fluid equivalences. Siberian Electronic Mathematical Reports 16, 2019, pages 826-862
Tarasyuk I.V., Buchholz P.
(Siehe online unter https://doi.org/10.33048/semi.2019.16.055)
