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.
In this paper we consider testing of reactive systems
. Reactive systems take inputs as well as provide outputs in form of spontaneous reactions. Testing of reactive systems can very naturally be
viewed as a two-player game between the tester and the implementation under test (IUT). Transitions are moves that may originate
either from the tester or from the IUT. The tester may use a
strategy to choose which of the inputs to apply in a given state.
We describe here a new online technique for testing reactive systems. In this approach we join test derivation from a model program
and test execution into a single algorithm. This combines the benefits of encoding transitions as method invocations of a model program with the benefits of a game-based framework for reactive systems. Test cases become test strategies that are created dynamically
as testing proceeds and take advantage of the knowledge gained by
exploring part of the model state space.
Formally, we consider model programs as implicit definitions of
interface automata and formulate the conformance relation between
a model program and a system under test in terms of alternating
simulation. This is a new approach for formalizing the testing of
The technique we describe was motivated by problems that we
observed while testing large-scale commercial systems, and the resulting algorithm has been implemented in a model-based testing
tool developed at Microsoft Research. This tool, called Spec Explorer [1, 7], is in daily use by several product groups inside of Microsoft. The online technique has been used in an industrial setting
to test operating system components and Web service infrastructure.
To summarize, we consider the following points as the main contributions of the paper:
The formalization of model programs as interface automata
and a new approach to using interface automata for conformance testing, including the handling of timeouts.
A new online or on-the-fly algorithm for using model programs for conformance testing of open systems, where the conformance relation being tested is alternating simulation.
The algorithm uses state dependent timeouts and state dependent action weights as part of its strategy calculation
Evaluation of the effectiveness of the theory and the tool for
the test of critical industrial applications.
The rest of the paper is organized into sections as follows. In
Section 2 we formalize what it means to specify a reactive system
using a model program. This includes a description of how the Spec
Explorer tool uses a model program as its input. Then in Section 3,
we describe the algorithm for online testing. In Section 4 we walk
through a concrete example that runs in the Spec Explorer tool. We
evaluate further sample problems and industrial applications of the
tool in Section 5. Related work is discussed in Section 6. Finally,
we mention some open problems and future work in Section 7
2. SPECIFYING REACTIVE SYSTEMS USING MODEL PROGRAMS
To describe the behavior of a reactive system, we use the notion
of interface automata [11, 10] following the exposition in . In-
stead of the terms “input” and “output” that are used in  we
use the terms “controllable” and “observable” here. This choice of
terminology is motivated by our problem domain of testing, where
certain operations are under the control of a tester, and certain op-
erations are only observable by a tester.
2.2 IUT as interface automaton
In the Spec Explorer tool the model program and the IUT are
both given by a collection of APIs in form of .NET libraries (or
dlls). Typically the IUT is given as a collection of one or more
“wrapper” APIs of the actual system under test. The actual system
is often multi-threaded if not distributed, and the wrapper is con-
nected to the actual system through a customized test harness that
provides a particular high-level view of the behavior of the system
matching the abstraction level of the model program. The wrapper
provides a serialized view of the observable actions resulting from
the execution of the actual system. It is very common that only a
particular aspect of the IUT is being tested through the harness. In
this sense the IUT is an open system.
... to read more articles, visit http://sqa.fyicenter.com/art/