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.
Showing items related by title, author, creator and subject.
What are we missing? a call for red teaming within the domestic maritime domain for anti-terrorism programs List, Timothy J. (Monterey, California: Naval Postgraduate School, 2015-12);As a component of the Department of Homeland Security and the department’s lead for maritime security, the Coast Guard is charged with executing theUnited States domestic maritime anti-terrorism program. It is critical ...
Using a modular open systems approach in Defense acquisitions: implications for the contracting process Rendon, Rene G. (Monterey, California. Naval Postgraduate School, 2005); NPS-CM-06-069The following article is taken as an excerpt from the proceedings of the annual Acquisition Research Program. This annual event showcases the research projects funded through the Acquisition Research Program at the Graduate ...
Using a Modular Open Systems Approach in Defense Acquisitions: Implications for the Contracting Process Rendon, Rene G. (2006-04-01); NPS-CM-06-069This research explores the use of the modular open systems approach (MOSA) as a method for implementing an evolutionary acquisition strategy as well as the implications of using such an approach on the contracting process. ...