Specification and Verification of Dynamic Communication Systems

Author

Bauer, Jorg ; Schaefer, Ina ; Toben, Tobe ; Westphal, Bernd

Author_Institution

Saarlandes Univ., Saarbrucken

fYear

2006

fDate

28-30 June 2006

Firstpage

189

Lastpage

200

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;

fLanguage

English

Publisher

ieee

Conference_Titel

Application of Concurrency to System Design, 2006. ACSD 2006. Sixth International Conference on

Conference_Location

Turku

ISSN

1550-4808

Print_ISBN

0-7695-2556-3

Type

conf

DOI

10.1109/ACSD.2006.29

Filename

1640236