Title :
Specification and Verification of Dynamic Communication Systems
Author :
Bauer, Jorg ; Schaefer, Ina ; Toben, Tobe ; Westphal, Bernd
Author_Institution :
Saarlandes Univ., Saarbrucken
Abstract :
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 demonstrated using a combination of model-checking and abstract interpretation. Our approach is illustrated using the application domain of car platoons
Keywords :
automobiles; formal specification; formal verification; message switching; queueing theory; specification languages; telecommunication network topology; traffic engineering computing; abstract interpretation; asynchronous communication; car platoon; dynamic communication system; formal verification; message queue; model-checking; specification language; Asynchronous communication; Communication system traffic; Communication system traffic control; Distributed control; Formal verification; Natural languages; Protocols; Specification languages; Topology; Traffic control;
Conference_Titel :
Application of Concurrency to System Design, 2006. ACSD 2006. Sixth International Conference on
Conference_Location :
Turku
Print_ISBN :
0-7695-2556-3
DOI :
10.1109/ACSD.2006.29
