Automating (specification ≡ implementation) using equational reasoning and LOTOS

Abstract

We explore some of the problems of verification by trying to prove that some sort of relationship holds between a given specification and implementation. We are particularly interested in the decisions taken in the process of establishing and formalising the verification requirements and of automating the proof. Despite the apparent simplicity of the original problem, the verification is non-trivial. The example chosen is an abstraction of a real communications problem. We use the formal description technique LOTOS [8] for specification and implementation, and equational reasoning, automated by the RIRL term rewriting system [9], for the proof.