Habilitation HABIL-2004-01

König, Barbara: Analysis and Verification of Systems with Dynamically Evolving Structure.
Universität Stuttgart, Fakultät Informatik, Elektrotechnik und Informationstechnik, Habilitation (2004).
238 Seiten, englisch.
CR-Klassif.F.3.1 (Specifying and Verifying and Reasoning about Programs)
F.4.2 (Grammars and Other Rewriting Systems)
Keywordsverification; static analysis; graph transformation

This thesis is concerned with verification and analysis techniques for software systems characterized by dynamically evolving structure, such as dynamic creation and deletion of objects, mobility and variable topology. Examples for such systems are pointer structures, object-based systems and communication protocols in which the number of participants is not constant.

The approach taken here is based on graph transformation systems, an intuitive and---at the same time---powerful formalism for the modelling of distributed and mobile systems. So far there exists comparatively little research concerning the verification of graph rewriting.

We will---in the first part of this thesis---introduce graph transformations and give an overview of existing analysis and verification methods, with a focus on the verification of systems with dynamically evolving structure. Then we will describe three original lines of research: behavioural equivalences, type systems and approximation by Petri nets, all of them concerned with the analysis of graph transformation systems.

The second part consists of eight refereed research papers treating the previously introduced analysis and verification techniques in depth.

Volltext und
andere Links
PDF (1909349 Bytes)
Abteilung(en)Universität Stuttgart, Institut für Formale Methoden der Informatik, Sichere und Zuverlässige Softwaresysteme
Eingabedatum22. Juli 2005
   Publ. Informatik