Static Analysis of Dynamic Communication Systems by Partner Abstraction

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.