Model-based Testing with SpecExplorer

Established: December 10, 2008

Spec Explorer is a software development tool for advanced model-based specification and conformance testing.

New Version of Spec Explorer as an extension to Visual Studio is now available: Spec Explorer 2010 (opens in new tab)

Encode a system’s intended behavior (its specification) in machine-executable form (as a “model program”). The model program typically does much less than the implementation; it does just enough to capture the relevant states of the system and show the constraints that a correct implementation must follow. The goal is to specify from a chosen viewpoint what the system must do, what it may do and what it must not do.
Explore the possible runs of the specification-program as a way to systematically generate test suites.
Compare the behavior of the model program to the system’s implementation in each of the scenarios discovered by algorithmic exploration. Discrepancies between actual and expected results are called conformance failures.

A confrmance error may indicate any of the following:

Implementation Bug. A code defect in the implementation under test [IUT].
Modeling error. A code defect in the model program itself.
Specification error. A mistake or ambiguity in the system’s specification (in other words, a misrepresentation of the intended system behavior).
Design error. A logical inconsistency in the system’s intended behavior.

Spec Explorer 2004 consists of:

The software modeling languages Spec# (opens in new tab) and AsmL (opens in new tab).
An explicit-state model checker, which allows the user to search the (possibly infinite) space of all possible sequences of method invocations that 1) do not violate the pre- and postconditions and invariants of the system’s contracts and 2) are relevant to a user-specified set of test properties.
A traversal engine, which unwinds the resulting finite state machine to produce behavioral tests that cover all explored transitions.
A binding mechanism allows users to associate actions of the model with methods of an implementation written .NET language. Both managed and unmanaged implementations may be tested if the .NET interop features are used.
A conformance checker that executes the generated behavioral tests. Alternatively, Spec Explorer supports an “on-the-fly” mode where test derivation (via model checking and traversal) and conformance checking of the implementation occur together.

The next generation of Spec Explorer is now available from: Spec Explorer 2010 (opens in new tab)

You can also use NModel (opens in new tab), which is is an open source model-based analysis and testing framework for model programs written in C#. It is explained and used in the book Model-based Software Testing and Analysis with C# (opens in new tab).

Principal Researcher

Learn more