Reference:

J. Bauer and Reinhard Wilhelm. Static Analysis of Dynamic Communication Systems. In 14th International Static Analysis Symposium, volume 4634. Springer, 2007.

Abstract:

Prominent examples of dynamic communication systems include traffic control systems and ad hoc networks. They are hard to verify due to inherent unboundedness. Unbounded creation and destruction of objects and a dynamically evolving communication topology are characteristic features.

Partner graph grammars are presented as an adequate specification formalism for dynamic communication systems. They are based on the single pushout approach to algebraic graph transformation and specifically tailored to dynamic communication systems. We propose a new verification technique based on abstract interpretation of partner graph grammars. It uses a novel two-layered abstraction, partner abstraction, that keeps precise information about objects and their communication partners. We identify statically checkable cases for which the abstract interpretation is even complete. In particular, applicability of transformation rules is preserved precisely. The analysis has been implemented in the hiralysis tool. It is evaluated on a complex case study, car platooning, for which many interesting properties can be proven automatically.

Keywords:

static analysis, graph transformation, communication topologies

Suggested BibTeX entry:

@inproceedings{BauWi07,
    author = {J. Bauer and Reinhard Wilhelm},
    booktitle = {14th {I}nternational {S}tatic {A}nalysis {S}ymposium},
    publisher = {Springer},
    title = {{S}tatic {A}nalysis of {D}ynamic {C}ommunication {S}ystems},
    volume = {4634},
    year = {2007}
}