Experience in developing and testing network protocol software using FDTs
This paper presents the research effort to formally specify, develop and test a complex real-life protocol for mobile network radios (MIL-STD 188-220). As a result, the team of researchers from the University of Delaware and the City College of the City University of New York, collaborating with scientists from CECOM (an R&D facility of the US Army) and the US Army Research Laboratory, have helped advance the state-of-the-art in the design, development, and testing of wireless communications protocols. Estelle is used both as the formal specification language for MIL-STD 188-220and the source to automatically generate conformance test sequences. The formal test generation effort identified several theoretical problems for wireless communication protocols (possibly applicable to network protocols in general): (1) the timing constraint problem, (2) the controllability problem, (3) inconsistency detection and elimination problem and (4) the conflicting timers problem. Based on the collaborative research results, two software packages were written to generate conformance test sequences for MIL-STD 188-220. These packages helped generate tests for MIL-STD 188-220s Data Link Types 1 and 4 services that were realizable without timer interruptions while providing a 200% increase in test coverage. The test cases have been delivered and are being used by a CECOM conformance testing facility.
formal specification mil-std 188-220 estelle conformance testing formal description technique protocol specification test case generation pacs