Naval Postgraduate School
Mushroom: a program for the automated verification of an SCM protocol specification
Article (502.8Kb)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 program 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 confirm these earlier results.
Description
The article of record as published may be found at http://dx.doi.org/10.1109/CNP.1993.340910
Collections
Related items
Showing items related by title, author, creator and subject.
-
Business case analysis of the Joint Strike Fighter's alternate engine program
(Monterey, California. Naval Postgraduate School, 2007-12);The Joint Strike Fighter (JSF) program is the largest Department of Defense (DoD) military aircraft acquisition program to date. The JSF will serve the Air Force, Navy and Marine Corps, as well as many of our key ... -
A protocol validator for the SCM and CFSM models
(Monterey, California: Naval Postgraduate School, 1993-06);This thesis introduces and describes a software tool called Mushroom which automates the analysis of network protocols specified by the Systems of Communicating Machines (SCM) and the Communicating Finite State Machines ... -
Lessons learned from the patrol hydrofoil missile (PHM) program
(Monterey, California. Naval Postgraduate School, 1979-03);The PHM project began as a major NATO acquisition program consisting of 60 or more ships for international purchase. Today the program consists of just 6 ships for the United States alone. This thesis reviews the history ...
