A protocol validator for the SCM and CFSM models
Loading...
Authors
Bulbul, Zeki Bulent
Subjects
Systems of Communicating Machines
Communicating Finite State Machines
SCM
CFSM
Protocol verification
Communicating Finite State Machines
SCM
CFSM
Protocol verification
Advisors
Lundy, G.M.
Date of Issue
1993-06
Date
June 1993
Publisher
Monterey, California: Naval Postgraduate School
Language
en_US
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 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.
Type
Thesis
Description
Series/Report No
Department
Department of Computer Science
Organization
Naval Postgraduate School (U.S.)
Identifiers
NPS Report Number
Sponsors
Funder
Format
136 p.
Citation
Distribution Statement
Approved for public release; distribution is unlimited.
Rights
Copyright is reserved by the copyright owner