Footnote:
Diese Datenquelle enthält auch Bestandsnachweise, die nicht zu einem Volltext führen.
Description:
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 ...