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