Automated Network Protocol Reachability Analysis with Supertrace Algorithm and TESTGEN: Automated Generation of Test Sequence for a Formal Protocol Specification.

摘要

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 cannot be analyzed efficiently by the full state search method. The 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. A 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 were consistent with the previous results. The automation of the tool expanded the applicability of the previous procedure to larger and more complex protocols. Supertrace, Network protocols, Reachability analysis, Conformance test, System of communicating machines Protocol model.