Testing an implementation's conformance to a formal specification: the SNR high speed transport protocol
Loading...
Authors
Grier, Robert Baxter
Subjects
Advisors
Lundy, G.M.
Date of Issue
1995-03
Date
March 1995
Publisher
Monterey, California. Naval Postgraduate School
Language
en_US
Abstract
The major problem addressed by this research is testing the actual implementation of a high speed networking transport protocol, SNR, written by two masters degree candidates, Wan and Mezhoud, to determine its adherence to a formal specification described by H. A. Tipici and G. M. Lundy. The approach taken was to modify the code to provide a program trace which included information about internal state variables and was designed to follow the specification's finite state machine description. The specification was used in conjunction with Testgen, a program written by C. Basaran, to generate a set of verification tests. A program was designed and implemented to provide a detailed analysis of the implementation, based on these two sets of data, to identify any deviations from the specification. The results of this work found machines T2, R1 and R2 perform the dequeuing of packets in unspecified states, and that R4 fails to check for an empty INBUF before finishing. The automated verification process enabled the detailed inspection of hundreds of lines of trace listings in seconds, providing information about which transitions were actually taken and error messages when failures to perform required actions occurred or predicate requirements were not met.
Type
Thesis
Description
Series/Report No
Department
Computer Science
Organization
Identifiers
NPS Report Number
Sponsors
Funder
NA
Format
65 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.