Online Testing with Model Programs

By:

ABSTRACT
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.

1. INTRODUCTION
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 reactive systems.

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 [10]. In- stead of the terms “input” and “output” that are used in [10] 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.

Full article...

Other Resource

... to read more articles, visit http://sqa.fyicenter.com/art/