Flick, Nils Erik (2016) Proving correctness of graph programs relative to recursively nested conditions. PhD, Universität Oldenburg.

Preview

Volltext (2254Kb)

Abstract

With graph programs, one can formally model the behaviour of a wide range of discrete systems. These programs extend graph rewriting by control structures (sequence, choice and iteration). This thesis presents a theoretically founded formalism for specifying properties of graph programs and a proof-based approach to verifying the partial correctness of a graph program relative to a pre- and postcondition. A novel specification language, recursively nested conditions (mu-conditions) is introduced, which can express nonlocal state properties and which is shown to be distinct from other relevant formalisms. The verification approach consists of: an adaptation of Dijkstra's weakest precondition calculus to graph programs and mu-conditions, a proof calculus for mu-conditions, whose core part is a rule schema for inductive refutation. Additionally, a formulation of correctness under adversity and structure-changing Petri nets are elaborated within the same framework.

["eprint_fieldname_title_plus" not defined]

Beweisverfahren für die Korrektheit von Graphprogrammen bezüglich rekursiv geschachtelter Bedingungen

["eprint_fieldname_abstract_plus" not defined]

Mit Graphprogrammen können viele Arten diskreter Systeme formal modelliert werden. Es sind Graphersetzungssysteme mit Kontrollstrukturen (Sequenz, Auswahl und Iteration). In dieser Arbeit werden ein theoretisch begründeter Formalismus zum Spezifizieren von Eigenschaften von Graphprogrammen sowie ein Verfahren zum Nachweis der partiellen Korrektheit von Graphprogrammen eingeführt. Rekursiv geschachtelte Graphbedingungen (mu-Bedingungen) sind eine neue Spezifikationssprache, die nichtlokale Zustandseigenschaften ausdrücken kann und sich nachweislich von anderen Formalismen unterscheidet. Der Verifikationsansatz besteht aus: einer Übertragung von Dijkstras Kalkül der schwächsten Vorbedingungen auf Graphprogramme und mu-Bedingungen, einem Beweiskalkül für mu-Bedingungen, dessen Kernstück ein Regelschema für induktive Widerlegung ist. Desweiteren werden innerhalb desselben Frameworks Korrektheit unter widrigen Umständen und strukturveränderliche Petrinetze betrachtet.

Item Type:	Thesis (PhD)
Uncontrolled Keywords:	Non-local graph conditions, graph programs, partial correctness, weakest precondition calculus, structure-changing Petri
Subjects:	Generalities, computers, information > Computer science, internet
Divisions:	School of Computing Science, Business Administration, Economics and Law > Department of Computing Science
Date Deposited:	22 Dec 2016 07:07
Last Modified:	22 Dec 2016 07:07
URI:	https://oops.uni-oldenburg.de/id/eprint/2895
URN:	urn:nbn:de:gbv:715-oops-29769
DOI:
Nutzungslizenz:

Actions (login required)

View Item