Formal Black Box Testing for Partially Specified Deterministic Finite State Machines

摘要

One of the most important methods of generating test sets for software modelled by finite state machines is Chow's W-method. However, the W-method is only proved to work if both the specification and the implementation are completely-specified deterministic finite state machines (i.e. there is a transition for any state and any input symbol). This paper extends the W-method to (possibly) partially specified deterministic finite state machines. It shows that, by slightly augmenting the test set, the W-method remains valid in this, more general, case. It is also shown how this generalised W-method can be used to generate test sets for a type of extended finite state machines, called stream X-machines (Eilenberg machines).