View article

This paper exploits design patterns employed in coordinating autonomous transport vehicles in order to ease the burden in verifying cooperating hybrid systems. The presented verification methodology is equally applicable for avionics applications (such as the traffic alert and collision avoidance system (TCAS)), train applications (such as the European train control system (ETCS)), or automotive applications (such as platooning). We present a verification rule explicating the essence of employed design patterns, 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 behaviour of the involved traffic agents, or by purely local proofs, involving only a single traffic agent. A companion paper will show how such local proof obligations can be discharged automatically.