Specification and Verification of Dynamic Communication Systems

Dynamic communication systems (DCS) are complex because of their unboundedness in several dimensions. They have an unbounded and changing number of objects, a dynamically changing communication topology and unbounded message queues for asynchronous communication. We present a specification language for DCS that captures these features but is still amenable for formal verification. The verification of relevant properties of DCS is demonusing a combination of model-checking and abstract interpretation. Our approach is illustrated using the application domain of car platoons.

• Type: Conference
• Year: 2006
• Where: ACSD
• Authors: Jörg Bauer, Ina Schaefer, Tobe Toben, Bernd Westphal
• Keywords: ACSD 2006, Communication Topology, Dynamic Communication Systems, Hardware, Unbounded Message Queues