Compositional verification of a communication protocol for a remotely operated aircraft

This paper presents the formal specification and verification of a communication protocol between a ground station and a remotely operated aircraft. The protocol can be seen as the vertical composition of protocol layers, where each layer performs input and output message processing, and the horizontal composition of different processes concurrently inhabiting the same layer, where each process should satisfy a distinct delivery requirement. A compositional technique is used to formally prove that the protocol satisfies these requirements. Although the protocol itself is not novel, the methodology employed in its verification extends existing techniques by automating the tedious and usually cumbersome part of the proof, thereby making the iterative design process of protocols feasible.

► A formal specification and verification of a communication protocol between a ground station and a remotely operated aircraft. ► A new compositional theory tailored to protocol verification. ► Proofs of invariant properties have been automated in the PVS strategy language.