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.
Lundy, Gilbert M.; Tipici, H. Alphan (IEEE, 1994-10);In recent years the emergence of optical fiber and its correspondingly high data rates have led to the development of much higher speed networks, both locally and over the long haul. These developments led to the design ...
Lundy, G.M.; Basaran, C. (IEEE, 1994-10);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 ...
Elmiro, Jose Luiz Timbo. (Monterey, California. Naval Postgraduate School, 1991-09);This research examines an improved FDDI protocol which ideally raises the network throughput from 100 to a maximum of 300 Megabits per second. It develops the details of the protocol structure at the MAC layer and provides ...