Testing a deterministic implementation against a non-controllable non-deterministic stream X-machine

A stream X-machine (SXM) is a type of extended finite state machine with an associated development approach that consists of building a system from a set of trusted components. One of the great benefits of using SXMs for the purpose of specification is the existence of test generation techniques that produce test suites that are guaranteed to determine correctness as long as certain well-defined conditions hold. One of the conditions that is traditionally assumed to hold is controllability: this insists that all paths through the SXM are feasible. This restrictive condition has recently been weakened for testing from a deterministic SXM. This paper shows how controllability can be replaced by a weaker condition when testing a deterministic system against a non-deterministic SXM. This paper therefore develops a new, more general, test generation algorithm for testing from a non-deterministic SXM.