Testing an implementation's conformance to a formal specification: the SNR high speed transport protocol
Grier, Robert Baxter
MetadataShow full item record
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.
RightsThis 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.
Showing items related by title, author, creator and subject.
Johnson, Jean; Blais, Curtis (2008-04-01); NPS-AM-08-034Data sharing is the information technology watchword of our time. Revolutions in information exchange and interoperability are underway in government and industry through policies on the strategic end to data standards on ...
Coyne, Kevin M. (Monterey, California. Naval Postgraduate School, 1996-03);The Electronic Warfare Integrated Reprogramming Database (EWIRDB) is the primary Department of Defense (DoD) approved source of electronic warfare (EW) data. Its utilization in the areas of battle planning and EW research ...
Fragkos, Georgios (Monterey, California. Naval Postgraduate School, 2002-09);Cyberspace is becoming the battlespace of the future, and military practices, like deception, seem to be suitable for defending information systems from attacks. In this thesis, we explore the concept of intelligent software ...