Spec Explorer Team Blog

Spec Explorer Webcast in German Online

In case you are capable of the German language, Christian Binder has posted an interview with me taken during TechED 2009 in Berlin, and we augmented it with an extended Webcast of using Spec Explorer, including its application by Microsoft for the Protocol Documentation Program. Check it out here!

How to customize test initialization and logging

Junfeng Dai has written an article about customizing Spec Explorer for using NUnit as the test execution engine instead of VSTT a few month ago. The same general approach can be used for simpler scenarios, for example to add custom test initialization code or test logging, which I would like to explain here.

When Spec Explorer generates test code, this code is placed in a class which derives from a base class found in the Spec Explorer runtime. You can simply insert a ‘middle man’ between this class and the generated test code class, overriding some methods.

Suppose you have created a Spec Explorer project based on the ‘static modeling solution’ (the same applies for any other Spec Explorer project), and you have generated test code.  You will see that the test code looks as below:

   1:  namespace SpecExplorer1.TestSuite {

   2:      using System;

   3:      using System.Collections.Generic;

   4:      using System.Text;

   5:      using System.Reflection;

   6:      using Microsoft.SpecExplorer.Runtime.Testing;

   7:      

   8:      

   9:      [System.CodeDom.Compiler.GeneratedCodeAttribute("Spec Explorer", "3.0.2168.0")]

  10:      [Microsoft.VisualStudio.TestTools.UnitTesting.TestClassAttribute()]

  11:      public partial class AccumulatorTestSuite : VsTestClassBase {

  12:          

  13:          public AccumulatorTestSuite() { 

  14:             ...

  15:          }

The class VsTestClassBase in line 11 is what we would like to substitute. However, in contrast to the full replacement scenario, we want to still use most of its functionality, and continue to run our tests under VSTT.

So we add a class to the test suite project as below, where we override a couple of methods from VsTestClassBase:

namespace SpecExplorer1.TestSuite
{
    public class MyTestClassBase : VsTestClassBase
    {
        public override void InitializeTestManager()
        {
            base.InitializeTestManager();
            Console.WriteLine("My test initialization executes now");
        }

        public override void CleanupTestManager()
        {
            Console.WriteLine("My test cleanup executes now");
            base.CleanupTestManager();
        }

        public override void Comment(string description)
        {
            Console.WriteLine("My test logging executes now: {0}", description);
        }

        public override void Checkpoint(string description)
        {
             Console.WriteLine("My requirement logging executes now: {0}", description);
        }

    }
}

In the methods InitializeTestManager and CleanupTestManager, we add custom test preparation and cleanup code. Note that it is imperative to call the base class here (unless you want to install your own test manager, which is usually not required).

Finally, we just need to tell Spec Explorer to use our new test class base when it generates test code, instead of the standard one. This is achieved by setting the switch TestClassBase in the Cord configuration:

   1:  /// Contains actions of the model, bounds, and switches.

   2:  config Main 

   3:  {

   4:      /// The two implementation actions that will be modeled and tested

   5:      action abstract static void Accumulator.Add(int x);

   6:      action abstract static int Accumulator.ReadAndReset();

   7:   

   8:      switch StepBound = 128;

   9:      switch PathDepthBound = 128;

  10:      switch TestClassBase = "MyTestClassBase";

  11:      switch GeneratedTestPath = "..\\TestSuite";

  12:      switch GeneratedTestNamespace = "SpecExplorer1.TestSuite";

  13:      switch TestEnabled = false;

  14:      switch ForExploration = false;

  15:  }

Regenerating test code and executing it finally yields in the following test log:

My test initialization executes now
My test logging executes now: reaching state 'S0'
My test logging executes now: executing step 'call Add(2)'
My requirement logging executes now: Add rule captured
My test logging executes now: reaching state 'S1'
My test logging executes now: checking step 'return Add'
My test logging executes now: reaching state 'S8'
My test logging executes now: executing step 'call Add(2)'
My requirement logging executes now: Add rule captured
My test logging executes now: reaching state 'S12'
My test logging executes now: checking step 'return Add'
My test logging executes now: reaching state 'S16'
My test logging executes now: executing step 'call ReadAndReset()'
My test logging executes now: reaching state 'S20'
My test logging executes now: checking step 'return ReadAndReset/4'
My test logging executes now: reaching state 'S24'
My test cleanup executes now

Using the exploration result object model: Basics

Several advanced users have expressed interest to process the test suite generated by Spec Explorer in a different way from the built-in test code generation. The Spec Explorer object model allows to do that. This article provides an introduction to its basic usage.

Whenever Spec Explorer performs an exploration – including a machine which generates test cases – the result is stored in a file ending in ‘.seexpl’. This file is in fact a zipped archive of several XML files representing the result of exploration. The content of this file is displayed under Visual Studio in the well-known graphical form, as shown below – from the far -- for the TestSuite machine of the SMB2 project which comes as a sample with Spec Explorer:

In addition to displaying this file in Visual Studio, it can be also processed with a user program – which we are going to demonstrate in this article.

To this end, the assembly Microsoft.SpecExplorer.ObjectModel contains all you need. Let’s use this to develop a little program which prints some statistics about exploration, the captured requirements, and the action sequences. To replay what we do, create a console application under Visual Studio and add the reference to the above assembly:

The object model is contained in the namespace Microsoft.SpecExplorer.ObjectModel:

using System;
using System.Collections.Generic;
using System.Linq;
using System.Text;

using Microsoft.SpecExplorer.ObjectModel;

namespace TransitionSystemDemo
{
    class Program
    {
      ...

The top-level object representing an exploration result is called a transition system. This stems from the fact that it actually represents the exploration as a set of states, and transitions between those states labeled with actions. The transition system is loaded by a class called TransitionSystemLoader. Our main method can therefore look as below:

static void Main(string[] args)
{
    if (args.Length != 1)
    {
        Console.WriteLine("usage: transitionsystemdemo <pathtoseexpl>");
        Environment.Exit(1);
    }
    try
    {
        var loader = new ExplorationResultLoader(args[0]);
        TransitionSystem tsys = loader.LoadTransitionSystem();
        Process(tsys);
    }
    catch (Exception e)
    {
        Console.WriteLine("failed: " + e.Message);
        Environment.Exit(2);
    }
}

The method Process will be defined later. Let us first examine how to print statistics about the transition system, a method which is called from within Process. We use a bit of LINQish magic to compute the ordered list of all requirements captured or assumed to be captured by the transition system:

static void PrintStatistics(TransitionSystem tsys)
{
    Console.WriteLine("{0} states ({1} initial), {2} steps",
        tsys.States.Length, tsys.InitialStates.Length, tsys.Transitions.Length);
    var captured =
        tsys.Transitions.Aggregate(
                new string[0] as IEnumerable<string>,
                (cs, tr) => cs.Concat(tr.CapturedRequirements).Concat(tr.AssumeCapturedRequirements))
                .Distinct()
                .OrderBy(x => x);
    Console.WriteLine("captured: ");
    foreach (var req in captured)
        Console.WriteLine("  " + req);
}

The transition system contains three central properties which build the hooks for traversing it:

• The property tsys.States (of type State[]) is the array of all states in the transition system. Every entry in this array is an object containing information such as the state label, state kind, etc.
• The property tsys.InitialStates (of type string[]) contains the array of state labels constituting the initial states of the transition system. If the transition system represents a test suite, these are typically the start states of each test case.
• The property tsys.Transitions (of type Transition[]) is the array of all transitions. Every entry in this array is an object containing information such as the source and target state labels, the captured requirements, and the requirements which are assumed to be captured by the adapter

Running this part of the program on the exploration result file of the TestSuite machine in the SMB2 project results in output as below:

This part was easy. The more tricky part is to compute sequences (which would correspond to test cases) from the transition system. The challenges are:

• We want to be able to run our program on arbitrary transition systems, and those may contain cycles. We will deal with this by just stopping once we have walked through a cycle.
• The transition system – even in the case of a test suite – may contain branches (more than one outgoing transition from a given state). We will deal with this by actually generating our sequences similar to patterns in a Cord machine. So if we have an action A which leads to a state where both B and C are possible, we will generate A;(B|C).

The code resulting from this design is below:

static void PrintPatterns(TransitionSystem tsys)
{
    foreach (var stateLabel in tsys.InitialStates)
    {
        Console.WriteLine("Starting in state {0}:", stateLabel);
        Console.WriteLine(ToPattern(tsys, new HashSet<State>(), GetState(tsys, stateLabel)));
    }
}

static string ToPattern(TransitionSystem tsys, HashSet<State> visiting, State state)
{
    if (state.RepresentativeState != null)
        // skip intermediate state
      return ToPattern(tsys, visiting, GetState(tsys, state.RepresentativeState));
    if (visiting.Contains(state))
        // Stop at cycle
        return "";
    visiting.Add(state);
    // compute successor
    var successors = GetSuccessors(tsys, state).Select(tr => ToPattern(tsys, visiting, tr)).ToArray();
    visiting.Remove(state);
    if (successors.Length == 0)
        // end state
        return "";
    else if (successors.Length == 1)
        return successors[0];
    else
        return "(" + string.Join("|\r\n", successors) + ")";
}

static string ToPattern(TransitionSystem tsys, HashSet<State> visiting, Transition tr)
{
    var continuation = ToPattern(tsys, visiting, GetState(tsys, tr.Target));
    if (continuation != "")
        return tr.Action.Text + ";\r\n" + continuation;
    else
        return tr.Action.Text;
}

static State GetState(TransitionSystem tsys, string stateLabel)
{
    return tsys.States.First(state => state.Label == stateLabel);
}

static IEnumerable<Transition> GetSuccessors(TransitionSystem tsys, State state)
{
    return tsys.Transitions.Where(tr => tr.Source == state.Label);
}

• Every state has a property RepresentativeState. The reason for that is related to the representation of symbolic transition systems, which goes beyond the scope of this article. In this context, whenever we visit a state which has a representative, we should just skip this state and continue with the representative instead.
• We pass a set of the states which we are currently visiting through the algorithm. This allows us to detect cycles.
• In order to print the action, we use tr.Action.Text. This is the same as shown in the labels of the graphical representation in Visual Studio. However, we should note that the action object has much more detailed information than just the action label text, which we don’t use here.
• In order to compute the State object associated with a state label, and the successor transitions of a state, we search the arrays in the transition system again and again. This is indeed way too inefficient, and in a real application, we would like to cache this information.

We will illustrate the result again using the example of the TestSuite exploration result from the SMB2 project. The result for one of the proper sequence cases looks as below:

This concludes this little demo. There are a number of features of the transition system which you can exploit which we haven’t shown. Among the coolest is probably is that all information about actions and action parameters can be converted on-the-fly into reflection information and LINQ expressions, allowing one to write a test executor directly based on the transition system. I may come back with an example for this in a later post.

You can find the full text of the demo program in the window below:

using System;
using System.Collections.Generic;
using System.Linq;
using System.Text;

using Microsoft.SpecExplorer.ObjectModel;

namespace TransitionSystemDemo
{
    class Program
    {
        static void Main(string[] args)
        {
            if (args.Length != 1)
            {
                Console.WriteLine("usage: transitionsystemdemo <pathtoseexpl>");
                Environment.Exit(1);
            }
            try
            {
                var loader = new ExplorationResultLoader(args[0]);
                TransitionSystem tsys = loader.LoadTransitionSystem();
                Process(tsys);
            }
            catch (Exception e)
            {
                Console.WriteLine("failed: " + e.Message);
                Environment.Exit(2);
            }
        }

        static void Process(TransitionSystem tsys)
        {
            PrintStatistics(tsys);
            PrintPatterns(tsys);          
        }

        static void PrintStatistics(TransitionSystem tsys)
        {
            Console.WriteLine("{0} states ({1} initial), {2} steps",
                tsys.States.Length, tsys.InitialStates.Length, tsys.Transitions.Length);
            var captured =
                tsys.Transitions.Aggregate(
                        new string[0] as IEnumerable<string>,
                        (cs, tr) => cs.Concat(tr.CapturedRequirements).Concat(tr.AssumeCapturedRequirements))
                        .Distinct()
                        .OrderBy(x => x);
            Console.WriteLine("captured: ");
            foreach (var req in captured)
                Console.WriteLine("  " + req);
        }

        static void PrintPatterns(TransitionSystem tsys)
        {
            foreach (var stateLabel in tsys.InitialStates)
            {
                Console.WriteLine("Starting in state {0}:", stateLabel);
                Console.WriteLine(ToPattern(tsys, new HashSet<State>(), GetState(tsys, stateLabel)));
            }
        }

        static string ToPattern(TransitionSystem tsys, HashSet<State> visiting, State state)
        {
            if (state.RepresentativeState != null)
                // skip intermediate state
              return ToPattern(tsys, visiting, GetState(tsys, state.RepresentativeState));
            if (visiting.Contains(state))
                // Stop at cycle
                return "";
            visiting.Add(state);
            // compute successor
            var successors = GetSuccessors(tsys, state).Select(tr => ToPattern(tsys, visiting, tr)).ToArray();
            visiting.Remove(state);
            if (successors.Length == 0)
                // end state
                return "";
            else if (successors.Length == 1)
                return successors[0];
            else
                return "(" + string.Join("|\r\n", successors) + ")";
        }

        static string ToPattern(TransitionSystem tsys, HashSet<State> visiting, Transition tr)
        {
            var continuation = ToPattern(tsys, visiting, GetState(tsys, tr.Target));
            if (continuation != "")
                return tr.Action.Text + ";\r\n" + continuation;
            else
                return tr.Action.Text;
        }

        static State GetState(TransitionSystem tsys, string stateLabel)
        {
            return tsys.States.First(state => state.Label == stateLabel);
        }

        static IEnumerable<Transition> GetSuccessors(TransitionSystem tsys, State state)
        {
            return tsys.Transitions.Where(tr => tr.Source == state.Label);
        }

    }
}

Static vs. Instance-Based Models

Many Spec Explorer users have asked the question of how and when to choose between static or instance-based at the time of creating a model.

The Base Solution Wizard (Visual Studio File menu -> New -> Project… -> Visual C# -> Spec Explorer Base Solution) shortly explains in its second step the difference between these two kinds of models, while leaving the choice to the user:

Spec Explorer Base Solution Wizard

So I figured it would be worth explaining the reasons to pick one or the other in this blog post. I’ve explained in a previous one two different ways to connect your test cases: directly or through a test adapter.

If you decide to go with the latter, the design of the test adapter itself is one place where the static-vs.-instance-based decision can be made. A static adapter can be used to control an instance-based SUT and vice-versa. The test adapter is just another component in your (testing) system. The rationale and constraints involved in this decision are the same one would take into consideration for designing any component in an object-oriented design. Moreover, this is not an all-or-nothing choice. Static and instance-based members can be combined in the same adapter as needed.

Action declarations in Cord configurations are used to connect the test cases to an external entity (either the SUT or an adapter). Generally, if your test cases will call static methods in the adapter or SUT, your actions will be static, whereas you will have instance-based actions if the methods to be called are instance-based. So the actual choice between static vs. instance-based actions is not really made by the modeler, but rather by whoever designs that external entity. Of course, they could be the same person, but would mean wearing two hats anyway.

The implication of having instance-based actions is that model steps will need to invoke the actions on objects that are not only known at model-exploration time, but also at test execution time. This means that the receiver of an instance-based action (“this” in C#) must have been the output of an action in a previous step. If a rule creates an object but doesn’t return it in its associated action, future steps will not be able to use it as a receiver.

Now a second choice point is reached when creating a model program. Spec Explorer allows mapping instance-based actions to static rule methods (and in some cases, the other way round). The usual recommendation is not to make this switch, as modeling static actions with static rules (and instance-based actions with instance-based rules) is usually more natural. But we’ve seen cases where a modeler doesn’t agree with the design choice made at SUT or adapter design time and believes better model clarity can be achieved by using a different approach for the rules.

The goal, as with any design, is to keep your model simple to understand and to maintain, while achieving the desired behavior.

Connecting Your Tests to an Implementation

Spec Explorer supports two topologies for connecting generated test cases to the implementation of your System Under Test (SUT). They can be either connected directly or through a test adapter.

Connecting them directly means to declare the actual methods and events of your implementation as actions in a Cord configuration (either one by one or using the “action all” option to extract them for the SUT). Consequently, the generated test code will call directly into your SUT and expect the events it raises. This option can only be applied to managed code implementations that expose an API rich enough to allow testability.

Direct Connection

A test adapter is a (fairly thin) software layer that sits between your test cases and your SUT. When you create a test adapter, you declare the adapter methods and events as actions in a Cord configuration instead referring directly to the SUT. As a result, the generated test code will call methods (and expect events) in the adapter. The adapter has the task of turning these calls into SUT calls, usually performing some translation or marshaling. This architecture must be used when the implementation is not managed, when the communication is remote, when there is a test infrastructure in the middle (for example, to control the SUT’s UI), to raise the level of abstraction of modeling and testing, etc. Adapters are a way to get around testing environments that otherwise would be hard to tackle by managed test code derived solely from modeling. Thus they greatly extend the power of Spec Explorer.

Connection through a Test Adapter

It is possible in both approaches that the modeler and the adapter or SUT implementer collaborate by agreeing on the action interface as a contract and then proceed in parallel: the modeler ultimately being a consumer of the agreed interface and the implementer being the provider of the functionality behind the interface. Only at generated test case run time must the adapter or SUT interface be ready for execution. The modeler would declare the actions in Cord as abstract and use rules in the model program and Cord scenarios to model expected system behavior.

The Spec Explorer Story on WG’s Logbook

I posted a personal account of the history of Spec Explorer on my blog: how it is related to AsmL, Spec#, NModel, etc. Take a look if you are interested.

What is Model-Based Testing?

I know there are people out there who found out about Spec Explorer 2010 as a great testing tool, but are wondering what all that "Model-Based Testing" buzz is about. If you are in this group, this post should be a good place to start.

Of course, you can also search the Web for Model-Based Testing (MBT, for short) and you'll find plenty of information, since MBT is not new or restricted to Spec Explorer. It's in fact the subject of ongoing academic research and an industrial practice that has been around for a while and is here to stay. Tools like Spec Explorer just make it easier to learn and to use, and generally more accessible to a larger audience.

So I'll cut to the chase and explain what MBT is and what it's used for. Model-Based testing is considered to be a lightweight formal method to validate software systems.

It's formal because it works out of a formal (that is, machine-readable) specification (or model) of the software system one intends to test (usually called the implementation or System Under Test, SUT).

It's lightweight because, contrary to other formal methods, MBT doesn't aim at mathematically proving that the implementation matches the spec under all possible circumstances. What MBT does is systematically generate from the model a collection of tests (a "test suite") that, when run against the SUT, will provide sufficient confidence that it behaves as the model predicted it would.

So the difference between lightweight and heavyweight formal methods is basically about sufficient confidence vs. complete certainty. Now, the price to pay for absolute certainty is not low, which results in heavyweight formal methods being very hard (sometimes prohibitively hard) to apply to real-life projects. MBT on the other hand scales much better and has been used to test life-size systems in huge projects, some of them inside Microsoft.

Here's a simplified diagram showing how MBT works.

Model-Based Testing in a Nutshell

The method starts from a set of requirements usually written in prose, sketches or just shared by the development team as tribal knowledge.

The first task in the process (#1) is to create a machine-readable model that expresses all the possible behaviors of a system meeting the requirements. This has to be done by humans and is arguably the most work-intensive step. A key ingredient to keep it manageable is to work at the right level of abstraction. That is, as a modeler you should focus on certain aspects of the system that will be tested (such as UI elements or API calls) and forget about the rest. Other models can be created for other system aspects, as long as each of them is kept at a clear abstraction level.

In the case of Spec Explorer, models are written as sets of rules in a mainstream programming language (C#), which makes the learning curve much less steep than tools that require learning an ad-hoc formal language. Spec Explorer runs as an add-on to the Microsoft Visual Studio integrated development environment, which provides extensive support for .Net languages such as syntax coloring, auto-completion and refactoring. A small but powerful configuration language called Cord (short for "Coordination Language") complements the C# code by providing features to combine models, generate test data and select certain scenarios that are especially relevant for testing.

I said authoring a model is the most work-intensive step in an MBT process, but it also has a big payoff! Just by trying to turn informal requirements into a machine-readable model you are very likely to discover inconsistencies and missing pieces in the requirements ("What on Earth is the system expected to do when I press the Esc key twice?") This is illustrated by flow #2, where feedback about the requirements is obtained from the model.

Once the model is in place, a Model-Based Testing tool such as Spec Explorer can do its magic. It can automatically take a model and generate standalone test cases from it (#3). Spec Explorer is among the MBT tools that generate complete test suites from a model, including both the inputs to be provided to the SUT and the expected outputs, also called a test oracle.

So the test cases automatically generated by Spec Explorer will run independently from the model, in a standard unit test framework, such as the one included in Visual Studio or NUnit. The tests will provide the test sequences (and data) to control (#4) the implementation. But they will also observe (#5) the results coming back from the system to compare them with the outputs expected by the model and issue a verdict (#6) of Pass or Fail, together with log information for diagnostics. Moreover, this execution of the test cases in lockstep with the SUT can be reiterated to reproduce bugs and debugged to understand what went wrong.

Of course such a verdict will provide feedback about the implementation (#7). After all, finding bugs or gaining confidence on the implementation is the goal of the whole thing, right? Well, yes and no. A failing test case might also mean that the implementation is behaving correctly, but an error was made while creating the model! Or perhaps the model faithfully reflects the documented requirements, but it was the requirements that were wrong to begin with! If this happens, you shouldn't freak out. One of the big advantages of MBT is it makes test suite maintenance much easier, when compared with manually written test cases. Just take the result as normal feedback about the model or requirements (#8), fix the model to convey the behavior actually expected from the running system, re-generate your test cases, and voilà! You are back on track. The previously failing test cases should now pass. Keith, Wolfgang and I have shown an example of this workflow in our Channel 9 video.

I hope this both satisfies your curiosity about Model-Based Testing and feeds your curiosity about Spec Explorer, at least enough to install it and start using it!

Welcome to the Spec Explorer Team Blog!

Spec Explorer is a Model-Based Testing tool from Microsoft. It extends the Visual Studio integrated environment with the ability to define a model describing the expected behavior of a software system. Using this model you can generate tests automatically for execution within Visual Studio's own testing framework, or many other unit test frameworks.

You write models in a mainstream programming language (C#), accompanied by configuration files in a scripting language called Cord (short for "Coordination Language").

The name Spec Explorer comes from its power to explore these models (aka specifications) in order to discover all the potential behaviors they define, and present a graphical view of the result. Although the outcome of an exploration can be huge, the Cord language provides a very intuitive way to reduce it by selecting scenarios relevant for testing. If you have encountered purely state oriented tools, you will find Spec Explorer has very effective ways to deal with the notorious "state explosion" problem.

Spec Explorer is the latest and greatest in a family of tools for Model-Based Testing, originating from Microsoft Research and backed up by many research articles and collaborations. Our full-fledged product engineering team in the Windows Server Division, distributed between Redmond and Beijing, carries on enhancing and supporting Spec Explorer in its current form.

Spec Explorer is being extensively used to test several Microsoft technologies and has been successfully applied to testing thousands of pages of Windows open protocol specifications, a huge project that took more than 250 person years.

Today we are super proud to ship Spec Explorer 2010 for the first time outside Microsoft through MSDN DevLabs!

We'll use this blog to post technical articles and share samples with our user community. We hope you download Spec Explorer, try it out, and let us know what you think on the project forum.

Thanks in advance on behalf of the Spec Explorer team.