Test case generation based on formal specifications in Estelle

This paper deals with the generation of conformance test sequences from specifications in Estelle. Our approach is to make the well-founded test generation methods based on finite state machines (FSM) applicable to specifications in Estelle. An algorithm is presented for transformation of Estelle modules into a form free of provided-clauses. The transformed modules allow to apply test generation methods based on the FSM model. Using this approach, it is possible to cope with test sequence generation for control and data flow and with test data selection. The transformation is feasible if the variables that occur in provided-clauses have finite, countable domains. For realistic protocol specifications, this condition is fulfilled most of the time. Multi-module specifications are decomposed into a set of partial specifications related to separate services before combining the modules into one composite module. The approach partially has been implemented as prototype tools