Protocol Validator for the SCM and CFSM Models

摘要

This thesis introduces and describes a software tool called Mushroom whichautomates 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.