Gieseking, Manuel (2022) Correctness of Data Flows in Asynchronous Distributed Systems: Model Checking and Synthesis. PhD, Universität Oldenburg.

Preview

Volltext (4Mb)

Abstract

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.

["eprint_fieldname_title_plus" not defined]

Korrektheit von Datenflüssen in Asynchronen Verteilten Systemen: Modellprüfung und Synthese

["eprint_fieldname_abstract_plus" not defined]

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.

Item Type:	Thesis (PhD)
Uncontrolled Keywords:	Asynchrones Verteiltes System; Modellprüfung; Synthese; Petri-Netz, Temporale Logik
Subjects:	Generalities, computers, information > Computer science, internet
Divisions:	School of Computing Science, Business Administration, Economics and Law > Department of Computing Science
Date Deposited:	17 Feb 2023 15:07
Last Modified:	17 Feb 2023 15:07
URI:	https://oops.uni-oldenburg.de/id/eprint/5688
URN:	urn:nbn:de:gbv:715-oops-57691
DOI:
Nutzungslizenz:

Actions (login required)

View Item