 |
|
 |
|
|
Static Analysis of Dynamic Communication Systems by Partner Abstraction
|
|
|
|
|
 |
|
|
held by: |
Jörg Bauer
|
|
|
|
schedule: |
Thursday 2008-01-10, 16:00 - 17:00 (MI 03.11.018)
|
|
|
|
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 is evaluated on a complex case study, car platooning, for which many interesting properties can be proven automatically. |
|
 |
|
|
 |
Contact
