Model-based Testing with SpecExplorer
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
What are the core ideas behind Spec Explorer?
- 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.
What is a conformance error?
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.
What components do belong to Spec Explorer?
Spec Explorer 2004 consists of:
- 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.
What is the Future of Spec Explorer?
The next generation of Spec Explorer is now available from: Spec Explorer 2010
This is the original research version: Spec Explorer (version 1.0.9520).
You can also use NModel, 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#.
Publications
2008
- Margus Veanes, Colin Campbell, Wolfgang Grieskamp, Wolfram Schulte, Nikolai Tillmann, and Lev Nachmanson, Model-Based Testing of Object-Oriented Reactive Systems with Spec Explorer, in Formal Methods and Testing, Springer Verlag, 2008
2007
- Margus Veanes, Colin Campbell, and Wolfram Schulte, Composition of Model Programs, in FORTE, Springer Verlag, June 2007
- Margus Veanes, Juhan Ernits, and Colin Campbell, State Isomorphism in Model Programs with Abstract Data Structures, in FORTE'07, Springer Verlag, June 2007
2006
- Wolfgang Grieskamp, Nikolai Tillmann, and Wolfram Schulte, XRT- Exploring Runtime for .NET Architecture and Applications, in Electr. Notes Theor. Comput. Sci., vol. 144, no. 3, pp. 3-26, 2006
2005
- Wolfgang Grieskamp, Nikolai Tillmann, Colin Campbell, Wolfram Schulte, and Margus Veanes, Action Machines - Towards a Framework for Model Composition, Exploration and Conformance Testing Based on Symbolic Computation, in Quality Software, 2005. (QSIC 2005). Fifth International Conference on , IEEE Computer Society, September 2005
- Andreas Blass, Yuri Gurevich, Lev Nachmanson, and Margus Veanes, Play to Test, in FATES 2005, Springer Verlag, July 2005
- Colin Campbell, Margus Veanes, Jiale Huo, and Alexandre Petrenko, Multiplexing of Partially Ordered Events, in TestCom 2005, Springer Verlag, June 2005
- Margus Veanes, Colin Campbell, Wolfram Schulte, and Nikolai Tillmann, Online testing with model programs, in ESEC/SIGSOFT FSE, ACM, 2005
- Margus Veanes, Colin Campbell, Wolfram Schulte, and Pushmeet Kohli, On-The-Fly Testing of Reactive Systems, no. MSR-TR-2005-05, January 2005
- Colin Campbell, Wolfgang Grieskamp, Lev Nachmanson, Wolfram Schulte, Nikolai Tillmann, and Margus Veanes, Testing Concurrent Object-Oriented Systems with Spec Explorer, in FM, Springer, 2005
- Andreas Blass, Yuri Gurevich, Lev Nachmanson, and Margus Veanes, Play to test, no. MSR-TR-2005-04, January 2005
- Dean Rosenzweig, Davor Runje, and Wolfram Schulte, Model-Based Testing of Cryptographic Protocols, in TGC, Springer, 2005
- Colin Campbell and Margus Veanes, Exploration with Multiple State Groupings, in Abstract State Machines 2005, 2005
2004
- Uwe Glässer, Yuri Gurevich, and Margus Veanes, Abstract Communication Model for Distributed Systems, in IEEE TRANSACTIONS ON SOFTWARE ENGINEERING, vol. 30, no. 7, pp. 1-15, IEEE Computer Society, July 2004
- Lev Nachmanson, Margus Veanes, Wolfram Schulte, Nikolai Tillmann, and Wolfgang Grieskamp, Optimal strategies for testing nondeterministic systems, in ISSTA 2004, ACM, 2004
- Wolfgang Grieskamp, Nikolai Tillmann, and Margus Veanes, Instrumenting Scenarios in a Model-Driven Development Environment, in Journal of Information and Software Technology, vol. 46, no. 15, pp. 1027-1036, Elsevier , 2004
- Mike Barnett, Wolfgang Grieskamp, Lev Nachmanson, Wolfram Schulte, Nikolai Tillmann, and Margus Veanes, Towards a Tool Environment for Model-Based Testing with AsmL, in FATES 2003, Springer Verlag, 2004
2003
- Wolfgang Grieskamp, Lev Nachmanson, Nikolai Tillmann, and Margus Veanes, Test Case Generation from AsmL Specifications, in ASM 2003, Springer Verlag, March 2003
- Mike Barnett, Wolfgang Grieskamp, Lev Nachmanson, Wolfram Schulte, Nikolai Tillmann, and Margus Veanes, Model-Based Testing with AsmL .NET, in 1st European Conference on Model-Driven Software Engineering, 2003
- Margus Veanes and Rostislav Yavorsky, Combined Algorithm for Approximating a Finite State Abstraction of a Large System, in ICSE 2003/Scenarios Workshop, 2003
2002
- Wolfgang Grieskamp, Yuri Gurevich, Wolfram Schulte, and Margus Veanes, Generating finite state machines from abstract state machines, in ISSTA 2002, July 2002
