Static Analysis of Dynamic Communication Systems
Prominent examples of dynamic communication systems include traffic control systems and ad hoc networks. 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.
Partner graph grammars are presented as an adequate specification formalism for dynamic communication systems. They are a variant of the single pushout approach to algebraic graph transformation 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.