Verifying trace equivalence of a shared-memory-style communication system
This paper describes a formal verification for a shared-memory-style communication system. We first describe two versions (i.e. abstract and concrete) of the communication system based on an I/O-automaton, which is a formal system for distributed algorithms. Then, we prove the concrete version can perform all the external operations of the abstract version. This result, together with a former result [3], leads to the equivalence of the two versions. The proof is done by Larch theorem prover, and is the ever largest case study using I/O-automata.
trace equivalence i/o-automaton theorem proving