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. 2021. Cham : Springer International Publishing, 2021 (2021), Seite 95-117 1 Online-Ressource(XI, 487 p. 146 illus., 59 illus. in color.)
Tools and Algorithms for the Construction and Analysis of Systems 1st ed. 2021. Cham : Springer International Publishing, 2021 (2021), Seite 381-388 1 Online-Ressource(XXI, 465 p. 91 illus.)
