Analysis and verification of systems with dynamically evolving structure

Abstract

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.

In einer Zeit, in der Software-Systeme immer komplexer werden und immer schwerer zu durchschauen sind, ist es wichtig, nicht nur Techniken zur Verfügung zu haben, mit denen man diese Systeme konstruieren kann, sondern auch Methoden, mit deren Hilfe man in Entwicklung befindliche oder bereits bestehende Systeme verstehen und analysieren kann.

Besondere Probleme ergeben sich dabei bei der Analyse von Systemen, die sich durch einen hohen Grad an dynamischen Strukturveränderungen auszeichnen. Darunter fallen das dynamische Erzeugen und Löschen von Objekten, Mobilität und variable Topologien. Dieses Verhalten tritt in der Praxis bei vielen Programmen und Systemen auf, so zum Beispiel bei Zeigerstrukturen auf dem Heap, bei objekt-orientierten Programmiersprachen und bei Kommunikationsprotokollen mit variabler Teilnehmerzahl.

In dieser Habilitationsschrift wird ein grundlegender Ansatz zur Analyse solcher Systeme verfolgt. Dieser besteht darin, diese Systeme zunächst mit einer einfachen, intuitiven und zugleich ausdrucksstarken Modellierungssprache zu beschreiben: Graphtransformations-Systeme. Mit diesen können Systemzustände als Graphen und Zustandsübergänge mit Hilfe von Graphtransformations-Regeln modelliert werden. Mit Hilfe von Graphtransformations-Systemen -- auch Graphersetzungs-Systeme genannt -- kann man auf direkte Weise genau die Charakteristika von Systemen mit dynamischen Strukturveränderungen beschreiben: Dynamik, Mobilität und variable Topologie.