A Protocol Validator for the SCM and CFSM Models
Abstract
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 the 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.... Systems of Communicating Machines, Communicating Finite State Machines, SCM, CFSM, Protocol Verification.
Document Details
- Document Type
- Technical Report
- Publication Date
- Jun 01, 1993
- Accession Number
- ADA268523
Entities
People
- Zeki B. Bulbul
Organizations
- Naval Postgraduate School