Abstract

The paper introduces a theoretical foundation for generating abstract test paths related to Petri net specifications. Based on the structure of the Petri net model of the system, we first define the notion of unobservable transition. Unless such a transition is unreachable, we prove that its firing is necessarily ensured by the firing of another transition (namely observable transition) of the Petri net. We show that the set of observable transitions is the smallest set that guarantees the coverage of all the transitions of the Petri net model, i.e., any set of firing sequences of the model, namely observable traces, involving all the observable transitions passes eventually through the unobservable transitions as well. If some unobservable transitions are mandatory to trigger the execution of a test sub-sequence, observable traces are completed with such transitions to enhance the controllability of the test scenario. In addition to structurally identifying observable (and unobservable) transitions, we mainly propose two algorithms: the first allows to generate a set of observable paths ensuring full coverage of all the system transitions. It is based on an on-the-fly construction of a hybrid graph called the symbolic observation graph. The second algorithm completes the observable paths in order to explicitly cover the whole set of system’s transitions. The approach is implemented within an available prototype, and the preliminary experiments are promising.