Stenning's Protocol Implemented in UDP and Verified in Isabelle

Compton, M.

This paper is about the mechanical verification of UDP based network programs. It uses the UDP portion of a formal model of the Internet protocols TCP (Transmission Control Protocol) and UDP (User Datagram Protocol). The model includes asynchronous message passing, message loss and host fail- ure. The model is based around the sockets library, the primary API used for writing UDP and TCP based applications. This paper demonstrates that formal, machine-checked, proof is possible in the UDP model by presenting the proof of a safety property for an implementation of Stenning's Protocol. The protocol is implemented in a fragment of the OCaml language, using the sockets library for UDP network communication. The entire development including the safety proof is carried out in the proof assistant Isabelle; this assures soundness. Thus this paper demonstrates that it is possible to machine verify very concrete representations of distributed programs in a detailed semantics that accurately reflects the programs execution environment. Previously only abstract representations of this protocol have been machine verified. The proof, based on an implementation, provides a contrast to other verifications.

Cite as: Compton, M. (2005). Stenning's Protocol Implemented in UDP and Verified in Isabelle. In Proc. Eleventh Computing: The Australasian Theory Symposium (CATS2005), Newcastle, Australia. CRPIT, 41. Atkinson, M. and Dehne, F., Eds. ACS. 21-30.

(from crpit.com) (local if available)