Mushroom: a program for the automated verification of an SCM protocol specification

Abstract

Systems of Communicating Machines (SCM) is a formal model for the specification, verification and testing of communication protocols, which has been used to specify and verify several well-known protocols. In this paper we discuss a program, called mushroom, which automates the analysis using the SCM model. The pro­gram generates either the system state analysis or the full reachability analysis. The automation of this model is expected to greatly facilitate the use of the model for protocol design and analysis. The program has been used to verify some theoretical results, serving to con­firm these earlier results.