Accession Number : ADA304548

Title :   Application of a Mechanical Verification System to a High-Speed Transport Protocol.

Descriptive Note : Master's thesis,

Corporate Author : NAVAL POSTGRADUATE SCHOOL MONTEREY CA

Personal Author(s) : Pederson, Carl M., Jr

PDF Url : ADA304548

Report Date : SEP 1995

Pagination or Media Count : 128

Abstract : The high speed transport protocol, SNR, has never been completely analyzed. SNR's design incorporates a novel feature, specifically, periodic and frequent exchange of state information to coordinate the actions of the transmitter and receiver. This innovation exploits the higher bandwidth of modern fiber optic networks to increase data transmission rates. Traditional methods used to verify SNR have been largely unsuccessful because of the protocol's inherit complexity. The protocol functions as an asynchronous concurrent system and for that reason we apply a mechanical verification tool called Murphi. The Murphi Verification System is used to verify two phases of SNR, the connection establishment phase and data transfer phase operating under Mode 0 (no error or flow control) and Mode 1 (flow control only). The connection establishment phase functions as intended. Murphi detected apparent design flaws in both Mode 0 and Mode 1 of the data transfer phase. Buffer overflow can occur in Mode 1. An unexpected termination of the connection by the receiver is possible in both modes. The feasibility of applying Murphi to verify communication protocols in general is also addressed.

Descriptors :   *COMPUTER COMMUNICATIONS, FIBER OPTICS, CONTROL, INFORMATION TRANSFER, DATA TRANSMISSION SYSTEMS, ASYNCHRONOUS SYSTEMS, THESES, TRANSPORT, TRANSMITTERS, DATA RATE, BANDWIDTH, COMPUTER PROGRAM VERIFICATION.

Subject Categories : Computer Systems Management and Standards
      Command, Control and Communications Systems

Distribution Statement : APPROVED FOR PUBLIC RELEASE