Formal design and testing of MIL-STD 188-220A based on Estelle

This paper describes the Estelle specification of MIL-STD 188-280A intranet layer as well as a methodology for generating test sequences for checking the conformance of a protocol implementation to its specification. The methodology for deriving test cases from an Estelle specification, which serves as input to test generation techniques, is presented. A Chinese postman tour is used to determine a minimum-cost tour of the transition graph for various transition types. Finally, the paper discusses several controllability and optimization issues that need to be addressed in test cases generation for the intranet and datalink layers of MIL-STD 188-220A.