Automated generation of protocol sequences from formal specifications
MetadataShow full item record
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 protocol is specified formally as a finite state machine with local and shared variables. The test program, called TESTGEN, finds all paths which may be taken through the FSM and generates a sequence of tests to check all these paths. Certain possible error conditions or difficult to test conditions are also detected by the program, and the test designer receives a warning message. The program is applied to a formal specification of the CSM NCD and FDDI protocols, generating a test sequence for both of these protocols.
The article of record as published may be found at http://dx.doi.org/10.1109/CNP.1994.344374
RightsThis publication is a work of the U.S. Government as defined in Title 17, United States Code, Section 101. Copyright protection is not available for this work in the United States.
Showing items related by title, author, creator and subject.
Raghuram, Devalla (Monterey, California. Naval Postgraduate School, 1992-09);A group membership protocol ensures agreement and consistent commit actions among group members to maintain a sequence of identical group views in spite of continuous changes, either voluntary or otherwise, in processors' ...
Bulbul, Zeki Bulent (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 ...
Automated network protocol reachability analysis with supertrace algorithm and TESTGEN : automated generation of test sequence for a formal protocol specification Basaran, Cuneyt (Monterey, California. Naval Postgraduate School, 1994-03);The automation of reachability analysis is an important step in verification of network protocols. The memory size needed for the full state analysis of complex protocols is usually very large and not available on most of ...