Proceedings of the First Workshop on Formal Methods in Software Practice, January 11, 1996., San Diego, California, USA
A case study in formal verification of concurrent/distributed software is presented. The study concerns the modular specification and verification of a remote task protocol. The verification methodology used is based on semantic equivalence checking and is applicable to systems with hierarchical architectures. To support the methodology, we extended the verification tool Spin with the ability to check a particular class of semantic relations,and the language Promela upon which Spin is based with a simple mechanism to specify external operations. The foundations of semantic equivalence checking are also discussed briefly.