A selective test sequence generation method for protocols (with application to LOTOS).

This thesis proposes a new approach for generating selective test sequences from a LOTOS specification. First, based on the functional characteristics and semantic properties of the LOTOS operations, a criterion called operational coverage is developed, whereby, each of the LOTOS operations is assigned a mandatory set of sequences involving the actions in its operands. In general, these action sequences are not executable. A method called SELECTEST is then proposed for generating executable test sequences which satisfy the coverage criterion. SELECTEST first determines the cover for the specified operation from which a set of guides are obtained, each denoted as a possibly nonexecutable rooted path lying in the hierarchy of the LOTOS specification and passing through the operator. The guides are used to greatly speed up the search for the executable test sequences over the Petri-net representation transformed from the LOTOS specification. The coverage and method have also been generalized to the case of covering a set of LOTOS operations. The application to the Alternating Bit Protocol is included to illustrate the approach