Automated network protocol reachability analysis with supertrace algorithm and TESTGEN : automated generation of test sequence for a formal protocol specification
Lundy, Gilbert M.
MetadataShow full item record
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 the systems. A controlled partial search algorithm 'Supertrace' is implemented in this thesis to analyze protocols that can not be analyzed efficiently by full state search method. Supertrace algorithm provided the analysis of large protocols by generating 80% to 95% more states and is much faster as total process time than full state analysis. Second problem addressed in this thesis is the improvement of conformance testing for protocol implementations. The 'conformance testing' is used to check that the external behavior of a given implementation of a protocol is equivalent to its formal specification. A previously created procedure for conformance test sequence generation is automated in this thesis by the ADA programming language. The software tool implemented, uses a protocol specified formally with systems of communicating machines and creates test sequences as output. The tool was applied to a formal specification of the CSMA/CD and FDDI protocols and the results obtained, was consistent with the previous results. The automation of the tool expanded the applicability of the previous procedure to larger and more complex protocols.
Showing items related by title, author, creator and subject.
Randall, Michael Alan (Monterey, California. Naval Postgraduate School, 1992-12);Due to the speed and complexity of communication networks being designed today, it is imperative to ensure that they operate correctly. Todays fiber optic networks, which can transmit billions of bits per second over ...
Wilson, Jeffery Dwane. (Monterey, California. Naval Postgraduate School, 2000);The Naval Postgraduate School is developing a Multilevel Secure Local Area Network (MLS LAN) that incorporates commercial-off-the-shelf client workstations to provide multiple users with simultaneous secure access to stored ...
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 ...