Application of a mechanical verification system to a high-speed transport protocol
Loading...
Authors
Pederson, Carl M.
Subjects
Advisors
Volpano, Dennis
Date of Issue
1995-09
Date
September 1995
Publisher
Monterey, California. Naval Postgraduate School
Language
en_US
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.
Type
Thesis
Description
Series/Report No
Department
Computer Science
Organization
Identifiers
NPS Report Number
Sponsors
Funding
Format
115 p.
Citation
Distribution Statement
Rights
This publication is a work of the U.S. Government as defined in Title 17, United States Code, Section 101. Copyright protection is not available for this work in the United States.