A Well-Defined Estelle Specification for the Automatic Test Generation

For The automatic test generation in conformance testing, the first step is to derive a single FSM (finite state machine) from the formal specification, which does not loose any semantics of the formal language. The nondeterminism, parallelism, and modular structure characteristics of the formal specification language make it difficult to derive such a basis directly from the formal specification. In this paper, characteristics of Estelle specification language are analyzed and a “well-defined specification,” a restricted form of an Estelle specification, is proposed based on the analyzed results to enable a direct derivation of a single reduced FSM—which is called a CFG (control flow graph)—from the specification written in Estelle. The derived CFG provides a basis for the automatic test case generation. Algorithms to test whether the specification written in Estelle is well-defined or not, and to generate the CFG from the well-defined specification, are developed. Finally, as an example, the proposed technique is applied to TP0 (Transport Protocol class 0) specification written in Estelle. In applying these algorithms to the Estelle specification, some guidelines are also suggested for the specification which is not “well defined.”