Test Generation for X-machines with Non-terminal States and Priorities of Operations

Testing methods aiming to demonstrate that an implementation behaves the same as a specification X-machine (extended finite-state machine) usually assume that (1) all states are terminal states and (2) there are no priorities associated with operations on transitions. The considered model for the machine is such that outputs for transitions leading to non-terminal states will be buffered and contents of buffers will only be made observable when terminal states are entered. The X-machine testing method has been extended in this work to handle such an extension of X-machines (EFSM).Priorities of operations determine the order in which guards of transitions are evaluated. This makes it possible to reduce the size of a test suite. For instance, if testing has shown that a transition with a specific guard g has been implemented from some state, then no lower-priority transition with a guard implied by g may ever be executed from that state. It is hence not necessary to test for the presence of such a lower-priority transition.