Analysis of communication topologies by partner abstraction

Abstract

Dynamic communication systems are hard to verify due to inherent unboundedness. Unbounded creation and destruction of objects and a dynamically evolving communication topology are characteristic features. Prominent examples include traffic control systems based on wireless communication and ad hoc networks. As dynamic communication systems have to meet safety-critical requirements, this thesis develops appropriate specification and verification techniques for them. It is shown that earlier attempts at doing so have failed. Partner graph grammars are presented as an adequate specification formalism for dynamic communication systems. They form a novel variant of the single pushout approach to algebraic graph transformation equipped with a special kind of negative application conditions: Partner constraints that allow to reason about communication partners are specifically tailored to dynamic communication systems. A novel verification technique based on abstract interpretation of partner graph grammars is proposed. It is based on a two-layered abstraction that keeps precise information about objects and the kinds of their communication partners. The analysis is formally proven sound. Some statically checkable cases are defined for which the analysis results are even complete. The analysis has been implemented in the hiralysis tool. A complex case study - car platooning originally developed in the California PATH project - is modeled using partner graph grammars. An experimental evaluation using the tool discovered many flaws in the PATH specification of car platooning that had not been discovered earlier due to insufficient specification and verification methods. Many interesting properties can be automatically proven for a corrected implementation of car platooning using hiralysis.

Aufgrund ihres unbeschränkten Verhaltens sind dynamisch kommunizierende Systeme schwierig zu verifizieren. Sie zeichnen sich durch unbegrenztes Erzeugen und Zerstören von Objekten sowie eine sich ständig ändernde Kommunikationstopologie aus. Funkbasierte Verkehrskontrollsysteme und drahtlose Ad-hoc Netzwerke sind bekannte Beispiele dynamisch kommunizierender Systeme. Da diese außerdem sicherheitskritischen Anforderungen genügen müssen, werden in dieser Arbeit Spezifikations- und Verifikationsmethoden für dynamisch kommunizierende Systeme entwickelt. Es wird gezeigt, dass frühere Versuche in dieser Richtung fehlgeschlagen sind. Partner-Graphgrammatiken stellen einen geeigneten Formalismus zur Beschreibung solcher Systeme dar. Sie bilden eine neue Form des "single pushout" Ansatzes für algebraische Graphtransformationen erweitert um besondere negative Anwendungsbedingungen. "Partner constraints", die speziell für die Spezifikation dynamisch kommunizierender Systeme entwickelt wurden, erlauben, Nebenbedingungen an Objekte und ihre Kommunikationspartner zu formulieren. Es wird eine neuartige Verifikationstechnik vorgeschlagen, die auf der abstrakten Interpretation von Partner-Graphgrammatiken beruht. Diese fußt auf einer Abstraktion, die präzise Informationen über Objekte und ihre Kommunikationspartner erhält. Die Analyse wird korrekt bewiesen, und es werden statisch erkennbare Fälle aufgezeigt, in denen die Analyse sogar vollständige Resultate liefert. Die Analyse wurde in dem hiralysis Werkzeug implementiert. Eine komplexe Fallstudie - "car platooning", welche ursprünglich im Rahmen des California PATH Projektes entwickelt wurde - wird durch Partner-Graphgrammatiken modelliert. Eine experimentelle Auswertung mithilfe desWerkzeugs deckte zahlreiche Fehler in der ursprünglichen Modellierung auf, welche ihre Ursache in unzureichenden Spezifikations- und Verifikationsmethoden haben. Viele interessante Eigenschaften eines verbesserten Modells konnten mittels hiralysis automatisch bewiesen werden.