Accession Number : ADA294478
Title : Testing an Implementation's Conformance to a Formal Specification: The SNR High Speed Transport Protocol.
Descriptive Note : Master's thesis,
Corporate Author : NAVAL POSTGRADUATE SCHOOL MONTEREY CA
Personal Author(s) : Grier, Robert B., Jr
PDF Url : ADA294478
Report Date : MAR 1995
Pagination or Media Count : 79
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.
Descriptors : *SPECIFICATIONS, *COMPUTER PROGRAM VERIFICATION, *CONFORMITY, TEST AND EVALUATION, AUTOMATION, VERIFICATION, MODIFICATION, THESES, VARIABLES, INTERNAL, ERRORS, COMPUTER NETWORKS, MESSAGE PROCESSING.
Subject Categories : Computer Programming and Software
Distribution Statement : APPROVED FOR PUBLIC RELEASE