On “Exploring alternatives for transition verification”

Duan and Chen (doi:10.1016/j.jss.2009.05.019) proposed two methods for constructing an input/output sequence (IOS) whose execution on an implementation N of a given deterministic finite state machine (DFSM) M tests that N can be interpreted as a DFSM properly implementing every individual state and transition of M. This paper shows that the methods and three earlier similar methods potentially introduce cyclic dependencies between the essential segments of the produced IOS, meaning that the IOS might fail to be a complete test under the default interpretation. It then proposes modifications provably preventing such cycles. All the methods assume that M is completely specified and strongly connected and possesses a distinguishing set and that N has at most as many states as M.

► Unsoundness is reported for three recently proposed test construction methods.
► The same problems are reported also for three earlier similar methods.
► Simple corrections are proposed and proven sufficient.