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.

The Spec Explorer system is being developed as a research project by the Foundations of Software Engineering Group at Microsoft Research in Redmond.

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

See the project member websites for more information on AsmL and AsmL-T, the precursors of Spec# and Spec Explorer, respectively.

Download

NEW You can now directly download the newest version of Spec Explorer from here. .

For AsmL users: the new version has much improved support for AsmL.

In case of questions or problems with this release, please send e-mail to asmldev at microsoft.com. But please note that Microsoft Research does not provide regular support for this tool.

Mailing List

There is a mailing list for discussing AsmL issues. It is now open also for discussing 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. At this point (10/2006), the traffic is low and the archive does not contain much information about Spec Explorer, which has been used until now mostly internally of Microsoft.