Automating (Specification = Implementation) using Equational Reasoning and LOTOS

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 RRL term rewriting system [9], for the proof. 1 Introduction The last few years has seen an increase in the use of formal methods in the design and analysis of computer systems. This has many benefits; one of which is being able to verify that certain properties hold of a system (or not, as the case may be). However, although formal methods are popular for specification, formal verification..