On the Verification of Cooperating Traffic Agents
Damm, W. and Hungar, H. and Olderog, E.-R.
Proc. FMCO '03: Formal Methods for Components and Objects
This paper exploits design patterns employed in coordinating autonomous transport vehicles so as to ease the burden in verifying cooperating hybrid systems. The presented verification methodology is equally applicable for avionics applications (such as TCAS), train applications (such as ETCS), or automotive applications (such as platooning). We present a verification rule explicating the essence of employed design patters, guaranteeing global safety properties of the kind a collision will never occur, and whose premises can either be established by off-line analysis of the worst-case behavior of the involved traffic agents, or by purely local proofs, involving only a single traffic agent. In a companion paper we will show, how such local proof obligations can be discharged automatically.
01 / 2004
inproceedings
LNCS 3188
77-110
