The characteristics of the 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 finite state machine-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.>