On-The-Fly Testing of Reactive Systems

On-the-fly testing is a technique in which test derivation from a model program and test execution are combined into a single algorithm. It can also be called online testing using a model program, to distinguish it from offline test generation as a separate process. We describe a practical on-the-fly testing algorithm that is implemented in the model-based testing tool developed at Microsoft Research called Spec Explorer. Spec Explorer is being used daily by several Microsoft product groups. Model programs in Spec Explorer are written in a high level specification language AsmL or Spec#. We view model programs as implicit definitions of interface automata. The conformance relation between a model and an implementation under test is formalized in terms of refinement between interface automata, and testing amounts to a game between the test tool and the implementation under test.