Online testing with model programs

Online testing is a technique in which test derivation from a model program and test execution are combined into a single algorithm. We describe a practical online 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 the high level specification languages 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. Testing then amounts to a game between the test tool and the implementation under test.