Executable test sequences with operational coverage for LOTOS specifications

LOTOS the language for temporal ordering specifications is a formal language standardization by ISO for specifying distributed systems. The authors present a new approach to selectively generating executable test sequences which cover designated operations of a LOTOS specification. An operational coverage criterion is proposed, in which each operation is covered by a mandatory set of action sequences characterizing the operation. In general, these action sequences are not executable. Based on a Petri-net representation of the LOTOS specification, an algorithm is proposed for generating executable test sequences. The selected cover is used to greatly speed up the search for such test sequences over the Petri-net