Accession Number:

ADA280788

Title:

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

Descriptive Note:

Master's thesis

Corporate Author:

NAVAL POSTGRADUATE SCHOOL MONTEREY CA

Personal Author(s):

Report Date:

1994-03-01

Pagination or Media Count:

101.0

Abstract:

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 CSMACD 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. Supertrace, Network protocols, Reachability analysis, Conformance test, System of communicating machines Protocol model.

Descriptors:

Subject Categories:

  • Computer Systems

Distribution Statement:

APPROVED FOR PUBLIC RELEASE


View the full text of this report