Spec Explorer is a software development tool for advanced model-based specification and conformance testing. Spec Explorer can help software development teams detect errors in the design, specification and implementation of their systems. The tool is intended to be used by software testers, designers and implementers.

The core ideas behind Spec Explorer are

• To 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.
• To explore the possible runs of the specification-program as a way to systematically generate test suites.
• To 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 and 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 consists of the following components:

• The software modeling languages Spec# and AsmL.
• 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.

• Colin Campbell
• Wolfgang Grieskamp
• Lev Nachmanson
• Wolfram Schulte
• Nikolai Tillmann
• Margus Veanes

Past summer interns:

• Jiale Huo (now at McGill University, Canada)
• Pushmeet Kohli (now at University of Oxford, UK)

• Model-Based Testing of Object-Oriented Reactive Systems with Spec Explorer. Colin Campbell, Wolfgang Grieskamp, Lev Nachmanson, Wolfram Schulte, Nikolai Tillmann and Margus Veanes. Technical Report, May 2005. [PDF]
• Online Testing with Model Programs. Margus Veanes, Colin Campbell, Wolfgang Grieskamp, Wolfram Schulte, and Nikolai Tillmann. In ESEC/FSE 2005 [PDF]
• Optimal Strategies for Testing Nondeterministic Systems. L. Nachmanson,  M. Veanes, W. Schulte, N. Tillmann and  W. Grieskamp. In ISSTA 2004, International Symposium on Software Testing and Analysis , July 2004. [PDF]
• Instrumenting Scenarios in a Model-Driven Development Environment. W. Grieskamp, N. Tillmann and M. Veanes. In special issue of the Journal of Information and Software Technology.

Download

You can download the last MSR version of Spec Explorer or Spec Explorer 2004 from here. .

For AsmL users: this version has much improved support for AsmL.

The next generation of Spec Explorer is being productized. Please check the homepage of Wolfgang Grieskamp for more information.

Mailing List

There is a mailing list for discussing AsmL issues. It is also open for discussing related Spec Explorer issues. You can add yourself to the list using the web or by sending email. (You can also remove yourself using the web or by sending email.) The web interface allows non-members to browse the archives.