A Verification Concept for SDL Systems and its Application to the Abracadabra Protocol

Starting from a purely functional description of a communication protocol, we present a method how correctness proofs including safety- and progress properties can be developed systematically with an automatic theorem prover. We show how a complex proof can be divided into smaller ones due to proof arguments typically occurring in the area of protocol verification. Experience with this method shows that proofs can be developed with an acceptable amount of work. 1.1. Introduction The objective we pursue with our work is to verify properties of communication protocols. We start with an automata based description of the protocol and a property p given in terms of firstorder logic. Due to Broy [Bro87,91] we model the behaviour of the protocol agents with functions over streams and the system behaviour with its least fixed point c. If we use this formalism, we can reduce the verification problem to a proof of the theorem lf(c) ® p(c). lf is a logical formula formalizing that c is the least ..