Die Korrektheit von IT-Systemen spielt aufgrund deren wachsenden Einbindung in unser alltägliches Leben eine zunehmend wichtige Rolle und ist nicht zuletzt für sicherheitskritische Systeme entscheidend. Die Modellprüfung und die Synthese stellen dabei zwei etablierte, vollautomatische Ansätze zur Entwicklung von korrekten Implementierungen aus mathematisch präzisen und eindeutigen formalen Modellen und Spezifikationen dar. In dieser Arbeit führen wir, basierend auf Petri-Netzen bzw. Petri-Spielen und CTL*, neue Modellierungs- und Spezifikationsformalismen ein, die es ermöglichen, Anforderungen an den unbeschränkten lokalen Datenfluss in asynchronen verteilten Systemen zu stellen. Wir stellen Lösungsalgorithmen für die entsprechenden Modellprüfungs- und Syntheseprobleme zur Verfügung, die trotz des unbeschränkten Datenflusses und des unvollständigen Wissens der Systemkomponenten über die Umgebung des Systems in kausalitätsbasierten Modellen, eine angemessene Komplexität aufweisen.
Due to the increasing integration of information technology into our daily life, the correctness of such systems plays a major role in their development and is crucial, not least in safety-critical situations. Model checking and synthesis represent two fully automated, push-button approaches for developing correct implementations from mathematical precise and unambiguous formal models and specifications. In this thesis, we introduce new modeling and specification formalisms based on Petri nets, respectively Petri games, and CTL* that enable correctness requirements on the unbounded local data flow in asynchronous distributed systems. We provide solving algorithms for the corresponding model checking and synthesis problems with a reasonable complexity, despite the unbounded data flow and the components' incomplete knowledge about their environment in causality-based models.
Application and Theory of Petri Nets and Concurrency 1st ed. 2022. Cham : Springer International Publishing, 2022 (2022), Seite 236–257 1 Online-Ressource(XIV, 393 p. 131 illus., 73 illus. in color.)
1 Online-Ressource(VIII, 219 p. 73 illus., 29 illus. in color.).
Computer logic; Artificial intelligence; Software engineering; Microprogramming; Special purpose computers
Model Checking, Synthesis, and Learning -- From Linear Temporal Logics to Büchi Automata: The Early and Simple Principle -- Cause-Effect Reaction Latency In Real-Time Systems -- Quantitative Analysis of Interval Markov Chains -- Regular Model Checking: Evolution and Perspectives -- Regular Model Checking Revisited -- High-Level Representation of Benchmark Families for Petri Games -- Towards Engineering Digital Twinsby Active Behaviour Mining -- Never-Stop Context-Free Learning -- A Taxonomy and Reductions for Common Register Automata Formalisms.
This Festschrift, dedicated to Bengt Jonsson on the occasion of his 60th birthday, contains papers written by many of his friends and collaborators. Bengt has made major contributions covering a wide range of topics including verification and learning. His works on verification, in finite state systems, learning, testing, probabilistic systems, timed systems, and distributed systems reflect both the diversity and the depth of his research. Besides being an excellent scientist, Bengt is also a leader who has greatly influenced the careers of both his students and his colleagues. His main focus throughout his career has been in the area of formal methods, and the research papers dedicated to him in this volume address related topics, particularly related to model checking, temporal logic, and automata learning.
Theoretical Computer Science and General IssuesSpringer eBook Collection
Theoretical Computer Science and General Issues ; 13030;
Model Checking, Synthesis, and Learning 1st ed. 2021. Cham : Springer International Publishing, 2021 (2021), Seite 1-7 1 Online-Ressource(VIII, 219 p. 73 illus., 29 illus. in color.)
