A verification concept for SDL systems and its application to the Abracadabra protocol

SDL is a specification language to specify distributed systems.
Especially it is suitable for communication protocols. In some
cases however it is not enough to describe just the behaviour of a
protocol, but there are formulated some additional properties as
requirements of the SDL system. A formalism convenient to describe

them is for example first order logic. Our approach is to prove
such properties with methods of automated reasoning after
transforming the SDL specification into a first order logic
specification. The proofs are done with the program verification
system Tatzelwurm, especially with its prover. Practical
experience shows that it is convenient to do a proof in two steps.
In the first step the behaviour of the system is calculated out of
the behaviour of the agents. The proofs of this step is
independent of the property to prove. In this report we give a
proof methods containing instructions how the arguments are
applied during these proofs. It is shown how reachability analysis
is done during a formal proof and how fairness arguments are
applied. The report contains two papers, where the first one
describes the formal basis of the method and shows the proof
... mehrobligations occurring verifying a communication protocol. The
second paper shows how some tedious tasks can be done more elegant
using rewrite rules and recursive equations. In the appendix we
give two examples out of the verification of the Abracadabra
Protocol.