Refining specifications in adaptive testing of nondeterministic finite state machines

This paper addresses testing of nondeterministic FSMs. An implementation FSM is allowed to be less nondeterministic than its specification, so the reduction relation between machines is the conformance relation. Execution of a given test needs to be adaptive to avoid application of unneeded input sequences, since the test can have different inputs depending on output produced by the implementation under test in response to previous input. To further reduce testing efforts during test execution, the paper suggests performing refinement of the specification FSM by removing traces absent in the implementation, which has already passed some subtest of a given complete (sound and exhaustive) test. The test execution process can be terminated as soon as the executed so far subtest is complete for the current refined version of the specification. The sufficient conditions formulated in the paper can be used for this purpose