A protocol validator for the SCM and CFSM models
Bulbul, Zeki Bulent
MetadataShow full item record
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 (CFSM) models. SCM is a formal model for the specification, verification and testing of communication protocols. This model was originally developed to improve the CFSM model which is a simpler and earlier Formal Description Technique (FDT). The program is developed as two separate programs in the Ada programming language. The first program automates either the system state analysis (Smart Mushroom), or the full global analysis (Big Mushroom) for a protocol specified by the SCM model. The second program called Simple Mushroom, automates to global reachability analysis for the CFSM model. Mushroom greatly facilitates the use of these models for protocol design and analysis. The run time and memory efficiency of a previous program was improved to allow the analysis of larger and more complex protocols. The program was also extended to accept up to eight machines (processes) in the protocol specification. The user interface of the program has also been improved. Mushroom has been used to verify some well known protocols specified by the SCM and CFSM models such as the token bus protocol, Go Back N and Lap-B data-link control protocol.
Approved for public release; distribution is unlimited
Showing items related by title, author, creator and subject.
Seveney, James Arthur; Steinberg, Guenter Peter (Monterey, California. Naval Postgraduate School, 1990-06);The U.S. Navy has recently embarked on a program called Next Generation Computer Resources (NGCR) whose aim is a cooperative effort between Navy and industry to field a set of state of the art computers for shipboard use ...
Canterbury, Michael G. (Monterey, California. Naval Postgraduate School, 1995-09);One problem associated with the Distributed Interactive Simulation (DIS) architecture is its limited ability to support real time, simulated engagements of more than 1000 entities. To solve this problem, it is necessary ...
Lundy, G.M.; Basaran, C. (IEEE, 1994-10);A program which takes as input the formal specification of a protocol using the formal model systems of communicating machines, and outputs a sequence of tests for an implementation of the protocol is discussed. The ...