Spec Explorer Team Blog

How to initialize the initial state from an external source

2011-08-02T07:10:59Z

We received several emails to ask how to initialize the initial state from an external source recently, this post introduces a good pattern to do it.

We can implement our own data loader to load data from external source, and use this loader to initialize the state. Note that since data loading method might involve native invocation, we’d better set our loader to native (more details can be found at http://msdn.microsoft.com/en-us/library/ee620483.aspx).

Here is an example:

Model.cs

using System;
using System.Collections.Generic;
using System.Text;
using System.Linq;
using Microsoft.Modeling;
using Microsoft.Xrt.Runtime;
using System.IO;

[assembly: NativeType(typeof(Sample.MyLoader))]
namespace Sample
{
    static class MyLoader
    {
        internal static Sequence<UserData> Load()
        {
            int i;
            UserData data;
            Sequence<UserData> dataSequence = new Sequence<UserData>();
            string[] contents = File.ReadAllLines("c:\\temp\\data.txt");
            for (i = 0; i < contents.Length; i=i+2)
            {
                data.Name = contents[i];
                data.Address = contents[i + 1];
                dataSequence = dataSequence.Add(data);
            }
            return dataSequence;
        }
    }

    public struct UserData
    {
        public string Name;
        public string Address;
    }

    static class ModelProgram
    {
        static Sequence<UserData> Data = MyLoader.Load();

        [Rule]
        static Sequence<UserData> ShowData()
        {
            return Data;
        }

        [Rule]
        static void Clear()
        {
            Data = new Sequence<UserData>();
        }
    }
}

Config.cord

using Sample;
using Microsoft.Modeling;

config Main
{
action abstract static Sequence<UserData> Adapter.ShowData();
action abstract static void Adapter.Clear();

switch StepBound = 128;
switch PathDepthBound = 128;
}

machine ModelProgram() : Main
{
construct model program from Main
}

And the data under c:\temp

Lisa
#5, Danling Street
Bob
Queen Square

Then we explore the ModelProgram machine, and get the exploration graph like:

Of course the data source is not limited to text files, you can design your own loader to make your model more powerful.

Please feel free to share your thoughts or other good approaches to initialize initial state.

Spec Explorer 2010 Release 3.5 now available!

2011-04-18T15:03:00Z

Spec Explorer 2010, Release 3.5 Now Available!

Spec Explorer 2010 Release 3.5

Hello! We are delighted to announce the newest version of Spec Explorer 2010, Release 3.5.

Spec Explorer 2010 Release 3.5 contains new features, improved documentation, plus over 60 bug fixes. It runs on the Visual Studio 2010 Professional level product and above.

What’s New in Spec Explorer?

This release contains new / enhanced features including:

· Model change detecting:

The model change detecting feature detects all model changes and decides if Spec Explorer needs to re-explore the model. For specific machines, if Spec Explorer detects any change in the model code, cord script files, or other inputs, or detects a tool version change, Spec Explorer will start a new exploration; otherwise, Spec Explorer will use existing exploration result files for current exploration viewing, test code generation, and user customized post processing. The UI has been updated to allow you to force Spec Explorer to re-explore the machines.

· Multiple machine processing:

Now you can select multiple machines in Exploration Manager and explore, generate test code, or perform post processing tasks on them. For multiple machine processing, Spec Explorer generates a summary including all information of the batch-processing.

· Cord context menu:

Spec Explorer adds a new context menu item “Go To Definition” in the Cord editor, which enables users to navigate to specific configurations and machines. This is part of an ongoing effort to improve the Cord editing user experience and the general integration of the tool with Visual Studio.

Where can you get it?

The Spec Explorer download can be found on the Spec Explorer home page on Visual Studio Gallery.
See the on-line Release Notes for the latest, more detailed description of installation requirements, major features, bug fixes and known issues. Further information can also be found on The Spec Explorer Forum, The Spec Explorer Team Blog, and the latest Spec Explorer Help Documentation is always available in the MSDN library.
Please note that Spec Explorer 2010 Release 3.5 runs only on Visual Studio 2010. The 90 day trial version of Visual Studio 2010 can be found at here.

We hope you enjoy this release and look forward to hearing feedback from the Spec Explorer community.

The Spec Explorer Team

Spec Explorer 2010 Release 3.4 now available!

2011-01-07T07:38:04Z

Spec Explorer 2010, Release 3.4 Now Available!

Spec Explorer 2010 Release 3.4

Hello! We are delighted to announce the newest version of Spec Explorer 2010, Release 3.4.

Spec Explorer 2010 Release 3.4 contains new features, improved documentation, plus over 50 bug fixes. It runs on the Visual Studio 2010 Professional level product and above.

What’s New in Spec Explorer?

This release contains new / enhanced features including:

Dynamic traversal: Dynamic traversal provides a new test case generation mechanism. It works by traversing the exploration result (with a user-customizable strategy) while invoking the corresponding actions on the system under test at test runtime.
Validation performance improvement: The performance of Cord validation has been greatly improved.
Exploration cleanup: This enhanced feature provides a post-exploration process to remove redundant states/steps.
Getting partial exploration result: If exploration time exceeds the value of switch ExplorationTimeout or you click the “Stop” button during exploration, a partially explored / cleaned-up result will be displayed.
Model program construct from multiple namespaces / types: This feature allows a model program to be constructed from a list of comma-separated model namespaces / types.
Fully-qualified-name support for static action invocations: Fully qualified names are used to distinguish different static action invocations with the same method name.
Validation task in SpecExplorer.exe: New task “Validate” has been added as a task in SpecExplorer.exe

Where can you get it?

The Spec Explorer download can be found on the Spec Explorer home page on Visual Studio Gallery.
See the on-line Release Notes for the latest, more detailed description of installation requirements, major features, bug fixes and known issues. Further information can also be found on The Spec Explorer Forum, The Spec Explorer Team Blog, and the latest Spec Explorer Help Documentation is always available in the MSDN library.
Please note that Spec Explorer 2010 Release 3.4 runs only on Visual Studio 2010. The 90 day trial version of Visual Studio 2010 can be found at here.

We hope you enjoy this release and look forward to hearing feedback from the Spec Explorer community.

The Spec Explorer Team

Spec Explorer 2010 Release 3.3 now available as a Visual Studio Power Tool!

2010-09-30T20:22:00Z

Spec Explorer 2010 Release 3.3

Hello again! We are proudly announcing the newest version of Spec Explorer 2010, Release 3.3. The next step has been taken from being resident on DevLabs to being a Power Tool on Visual Studio gallery where you can find the new home page for Spec Explorer.

Spec Explorer 2010 Release 3.3 contains new features, continued improvement in documentation, plus over 100 bug fixes.

What’s New in Spec Explorer?

New features added in Release 3.3 include:

On-The-Fly (OTF) testing: On-The-Fly testing provides a new means to use Spec Explorer to create and run tests directly from models (machines). In On-The-Fly testing, the selection and evaluation of model actions (including events) is alternated with execution by the System Under Test/adapter.
Visual state search: This new feature in the Spec Explorer view enables the search for and highlighting of specific states.
Probe logging: Newly provided recording of probe values in states enhances analysis of test logs.
Test method customization: New control of test attributes in generated test code offers expanded support for other test frameworks in addition to the default one provided by Visual Studio.

Additionally, a Spec Explorer extension for UML is also being released at this time that is not included in the main Spec Explorer MSI and must be downloaded separately. Documentation for the UML extension can be found here.

Where can you get it?

The Spec Explorer downloads can be found on the Spec Explorer home page on Visual Studio Gallery.
See the on-line Release Notes for the latest, more detailed description of installation requirements, major features, bug fixes and known issues. Further information can also be found on The Spec Explorer Forum, The Spec Explorer Team Blog, and the latest Spec Explorer Help Documentation is always available in the MSDN library.
Please note that Spec Explorer 2010 Release 3.3 runs only on Visual Studio 2010 Professional Edition or higher. The 90 day trial version of Visual Studio 2010 can be found at here.

We hope you enjoy this release and look forward to your help by feedback and community involvement to continue making Spec Explorer better and better.

The Spec Explorer Team

The Controlled Calculator: An example of combining models while showing other features of Spec Explorer

2010-07-06T21:16:06Z

The Calculator

The core calculator model is a simple four function calculator. But infix calculators aren't entirely simple, because calculators demonstrate rich variations in outputs depending upon the exact order of input sequences of numbers, operations, and pressing the Equals keys. This implementation (and model) emulates the Windows Calculator. It is similar to but is slightly different from most store-bought calculators, especially in how the Equals key first repeats upon multiple key pushes and how an operation is done when only one operand has been provided. The model and implementation provided, however, should match up with the Windows calculator found under Accessories in the Windows Start menu. The Visual Studio 2010 solution for this example can be found here.

The Scenario

For the purposes of this sample, first the calculator functionality was created as a standalone product. This was then integrated with connection access that allowed the calculator to be used as a service. These were then modeled together as single integrated service. The calculator service model can be explored by itself and its implementation can optionally be tested standalone. The security authorization model controls access to the calculator via a simple minded Access Control List (ACL) consisting of a list of authorized users. (Note that the full ACL target resources and operations were not of interest for testing purposes so were not modeled). This simplified ACL was modeled on its own and can be explored on its own. Testing the ACL implementation requires the calculator service only for its connection capabilities.

How the Two Model Program Rule Sets Work Together

The ACL (authorization) model and the calculator service model actually synchronize on only a few actions, specifically connection and disconnection. They interleave the rest. The two model programs use the |?| operator to achieve this. Thus the authorization model can manage its ACL, allow and release user authorization on its own, as shown by exploring machine AuthorizationSlice, while the calculator model independently can do all of its calculator functionality (actions and events) . The vast majority of the all-important security related sequencing is done by transition modes in the authorization model. By carefully controlling when the synchronized actions (connect and disconnect) can occur the authorization model imposes the majority of inter-model sequencing constraints expressed by the joint model. Internally within the calculator service, however, the rules are generally aware that they must be connected to be enabled but have no knowledge at all of the authorization rules.

The end-to end-control is shown, not surprisingly, by machine EndToEndControl (Slice and Test) in the Cord file. It specifies that between ACL creations and disposals, users can be authorized multiple times, and between multiple authorizations the current user can connect multiple times, and within a connection multiple operations can be performed. This models the functionality of the core authorization sequences. Multiple simultaneous users and connections were not modeled. Had this been a test objective, likely instance based modeling would have been used and the implementation would be have been multithreaded. The current model (and the current implementation) adequately tests basic end-to-end functionality.

How the Implementation Does This

The implementation is written as four layers. The top level static class acts as the interface that implements the controllable and event actions declared in Cord. Thus it can be considered to be an adapter layer. The rest of the implementation is written as three layers, each of which is represented by a single object. There is an object that implements all of the calculator functionality, one that manages the connection to the calculator object, and finally one that represents the ACL control logic. In principle, the calculator object could be replaced by the real Windows calculator, but that has not been attempted.

Things to look for

In addition to modeling the active (behavioral) joining of two rule sets, this sample illustrates several important features of using Spec Explorer.

Cord

The Cord file is structured around logical groups of configurations, which of course is what configs are supposed to do for a living. The use of parameters in machines is shown by the DoubleOperand machine. The machines related to test purposes are built up from scenarios to model slices to test cases. For example, BigLongScenario to BigLongSlice to BigLongTest. There are a number of helper machines such as FullStart, CloseDown, SingleOperation. Fairly rigorous testing of calculator key sequences is shown by all the scenarios that are included in AllOperationsTogetherSlice (and Test).

But in many ways the most interesting machines deal with constructing and joining the two rule sets. The machine called AuthorizationSlice builds the (sliced) ACL model program and CalculatorService constructs the model program of the calculator service. These two model programs are actually independent of each other and use their own rule sets kept for convenience in separate name spaces and files. They make no assumptions about each other.

Machine JointModel is the one that joins the two by means of the partially synchronizing |?| operator, aka the “synchronized-interleaved parallel composition operator”. This synchronizes when both machines try to produce the same action just like the parallel synchronization operator ||-- in this case the connection and disconnection related actions--but interleaves otherwise when either machine produces an action unique to itself, just like the ||| operator. It may be that |?| is one of the more underappreciated operators in Cord. There are subtleties in its definition, but it is behaviorally powerful as shown.

Machine SimpleDirectSlice (and Test) deserves quick mention. If uncommented in CalculatorService.Connect (file Calculator.cs), the implementation will allow the calculator service to be tested on its own by automatically creating an ACL and authorizing a fictitious user. (The users defined for model slicing in configuration Authorize are neither fictitious nor necessarily innocent but that's another story.) This implementation short circuit would ordinarily be a security hole, since the ACL logic is being neutered, but is useful for testing and illustrates one way to get around the layering of the implementation code. Note that no changes were necessary in the CalculatorServiceModel rules to make this test generation work correctly because those rules by themselves do not depend on the ACL logic to which they are later composed only by the |?| operator

Model and Implementation Code

The model and implementation code is heavily commented and largely self-explanatory. The model code uses helper functions extensively. In both the model code and the implementation, state data is initialized actively in a constructor or other method. This promotes consistency and successful re-running of the same code in a test sequence or between test case executions.

Note that a rule may be blocked from producing a step in a helper function such as in CalculatorServiceModel.RequiresConnected (in file ArithmeticRules.cs). A rule method must reach all the way to an exit point without violating any Condition class constraints in order for any step(s) to be produced. Otherwise that rule execution is completely discarded during exploration and no step is produced outgoing from the current state by that rule.

In the same model rule set, the rule for the Divide action shows how a special condition, often an exception, can be converted into the expectation of a following event. Spec Explorer actions are indivisible which means they cannot suddenly be stopped and switched to another one. But at model evaluation time, the new state can reflect that a condition has occurred in the prior step (from a prior rule firing). In this case, the rule for OperationError will pick up on that fact that previously Divide had found and marked that the denominator was zero. A quick look at the configuration called Operation in Cord shows that the OperationError action is to be treated as an event. This is the only place to find out that the OperationError rule described an event, as it does not matter to the rule itself whether it is an input or output action to the SUT. Rather, the rule just knows under what conditions that the step can be seen externally to the SUT. It does matter, of course, to exploration and test code generation both of which will treat the event appropriately (which is why the Cord code tells them).

The actual implementation of the OperationError event can be found in CalculatorService (in file Calculator.cs). Notice it requires an instance of the correct name (OperationError) of a correct kind of delegate type. In this case it happens to be called OperationErrorHandler, but the type name may be chosen at will. The event is actually raised in this sample by helper method CalculatorService.RaiseError which is a callback used by the calculator object if it encounters a problem with divide by zero. The event will be placed on Spec Explorer's run time event queue for future consideration and the Divide action will run to completion, returning a zero value if a problem occurred as tested by scenario DividebyZero in Cord. When the model indicated the event would be eligible for consideration the queue will be examined and in the two cases of the ZeroDivide scenario it will be found. The third case does not look for the event and shows that a test may conclude successfully in an accepting state even if there are events left on the event queue.

Part of the moral of this story is that controllable actions (that is, inputs to the SUT) in the implementation are simple methods, but observable actions (that is, events) are implemented quite differently (as described above). Whereas in the rules, such actions are indistinguishable. And only in Cord, as the bridge in between, does Spec Explorer learn which is supposed to be which.

Actions, Step and Rules

2010-04-22T01:33:27Z

These are key concepts in Spec Explorer. Unfortunately sometimes they are used almost interchangeably. For now, let's clear up what they are and how they differ. To be fair, our documentation does a good job of using the correct terms but even so it pays to keep in mind their particular meaning.

Actions

In the most general notion, an action describes an interaction with the System Under Test (SUT) as seen from the tester's (or test system's) perspective. Spec Explorer recognizes three kinds of atomic actions that are discrete and indivisible: events, call actions, and return actions. Events represent autonomous messages coming from the SUT. A call action represents a stimulus from the test system to the SUT (as originally decided in the model). A return action must always follow after a call action without any intervening actions. The return actions capture the response (if any) from the SUT.

For further reference see Actions in the on-line documentation.

Action Declarations

Actions are declared in Cord configs using definitions that are like C# signatures preceded by the keyword "action". Cord expects the target SUT assemblies, or the adapter assemblies that wrap access to the SUT, to provide the .Net code that corresponds to each action. Put another way, the code to implement actions ultimately belongs not to the model but rather to the implementation to be invoked at test run time only.

An action declaration in Cord is always one of two kinds: a synchronous action declaration, which is the default, or an explicitly stated event action declaration. A synchronous action declaration actually forms the indivisible pair of an atomic call action followed by the corresponding atomic return action. The target of a call/return pair is implemented by a single method in the SUT, or the adapter to the SUT. Tests generated from Spec Explorer models invoke these methods on the SUT, and block waiting for them to return.

Event action declarations describe a single atomic action that indicates the SUT has sent a message on its own in keeping with the .Net event model. Events are implemented as standard C# events in the SUT (or adapter). Tests generated from Spec Explorer models subscribe to these events and add them to a queue as they arrive. Events from this queue are consumed when the test reaches a point where one or more events are expected.

Action Invocations

In Cord the use of an action in a behavioral (regular) expression is called an invocation, e.g. Add(1,2)/3. The arguments of an invocation can be variables or literals. Action invocation arguments, if specified, must always match in type and position with the signature provided by the action declaration in the applicable Cord config. Cord allows for polymorphic overloading of action declarations and Spec Explorer will chose the correct action declaration accordingly.

Note: action invocations do not directly call the implementation because they belong to the modeling. The implementation only becomes available at test execution time. Action invocations are also used to annotate rules, which are the other major part of modeling.

For further reference see Invocation in the on-line documentation.

Steps

Steps are the transitions in the graph. Step labels are action invocations that appear as transition (edge) labels in the exploration result graph.

At test run time, these step labels are translated into either method calls to the SUT (or adapter) that implement the call/return pair, or expected events. For call/return pairs, the generated test code will call the implementation (or adapter) method (call action step). The test code then will note the response with the actual out and result values given by the SUT (return action step). For events coming from the SUT (or adapter), all parameters will be considered as outputs. The actual values found at run time (for out parameters, results and event parameters) will be compared to the expected values from the model ("the oracle"). Only if these values meet all corresponding conditions will the test case succeed.

Like all behavioral modeling, Spec Explorer is ultimately interested in what can actually be seen in terms of inputs and outputs to the System Under Test (SUT), i.e. the actions. Everything else in Spec Explorer exists just to determine the legal sequence of steps (behavior) that a compliant SUT will be expected to follow in a test case. Even Spec Explorer's advanced notion of "state" is used only at modeling (exploration) time by a rule (see below) to determine if a particular step label would be permitted at that point in the sequence, but state does not partake in the actual test execution. Only step labels interpreted as invocations to the SUT (or adapter) and events are relevant to testing, as just described above.

Rules

Rules determine what steps can be produced leading from the current state in the model program. All rules are tried out by exploration from each state.

In Spec Explorer, rules are represented by model program methods that have been marked with the Rule attribute. The Rule attribute has an optional Action argument that specifies the action invocation.

Since rules exist to specify what steps the model program allows from a given state, the true output of a rule is zero or more step labels representing possible next actions from that state. Because of advanced features in Spec Explorer such as domains and parameter generation, it quite possible for a single rule to yield multiple instances of step labels for a given state. Of course a particular rule method always produces the same kind of step label in keeping with the Cord action declaration that matches the action invocation of its Rule attribute, but each step label will have a different combination of parameter values.

When a rule method is explored in order to generate step labels, the action invocation contained in its Rule attribute is used to map the exploration supplied input values to the rule method and to map back out/result values after the rule method has executed (as discussed below). A step label that cannot be produced by a rule due to violating a constraint in a Condition class method (e.g., Condition.Istrue) is simply discarded and will not appear in the exploration graph.

The action invocation in the Rule attribute is used to establish the correspondence between the Cord action declaration signature and the potentially different rule method signature in a way that is quite unique to Spec Explorer:

The name of the action invocation annotating a rule does not need to match the name of the rule method. It must however match the name of an action declaration in the Cord config that the model program is constructed from (e.g. "construct model from MyConfig").
Remember that action invocation arguments must always match in position and type compatibility with the corresponding action declaration signature in Cord.
If an action invocation argument is a literal value (for example, a number) it is not mapped at all to the rule method parameters! The rule method may simply assume what it wants when the action invocation parameter has that value without having to explicitly test for it.
If an action invocation argument is a variable rather than a literal value, it is mapped by name only, not by position, to the corresponding rule method parameter. If no such mapping is possible a validation error occurs. The type of the rule method parameter must agree with the corresponding type in the Cord definition. This includes the special names that can be used as action invocation arguments: "this" (represents the receiver of an instance-based rule method) and "result" (represents the return value of a non-void rule method). Note that the apparent return value of a C# rule method simply maps to the "result" output parameter.
All parameters of a rule method must appear in the action invocation annotating it. If one or more of the rule parameters do not appear in the corresponding action invocation, a validation error will result. This includes the special parameters "this" (for instance-based rules) and "result" (for non-void rules). For Example,

In Cord:

action abstract Sum(int x);

In Model Program:

static int stateTotal;

         [Rule(Action = "this.Sum(op) / result")]

   int AddtoTotal(int op) {

   return stateTotal += op;}
If the Action keyword is not specified in the rule annotation (e.g. "[Rule]"), Spec Explorer will automatically construct an invocation based on the rule method signature. The method name of the rule will be used as the action name (which must then match an action declaration in the corresponding Cord config), and the method's parameter names will be used as the action invocation parameters. For example, if the method signature is "int MyMethod(string name, float age)", the constructed action invocation will be "Action = "this.MyMethod(name,age)/result".

Summary: The action invocation in the Rule attribute must match in type and position (but not necessarily in name) the signature of the Cord action declaration. Rule method parameters must match the action invocation in the Rule attribute in name and type, but not necessarily position.

An Example

Action Declaration in Cord:

action abstract static bool Login(string user,int securityLevel);

Rules in the Model Program

The rule for a power user at security level 1 to login successfully (if unknown user, the rule itself fails, i.e. the action label will not be produced).
The rule for a power user at security level 1 to login unsuccessfully (if unknown user, the rule fails).
The rule for a normal user at any other security level allows login only if the user is already known and legal security levels also must be a positive integer value.

public static class MyModel

{

static bool loggedIn; // State variable for Login status

static string userName; // current user id with prefix

static int securityRing; // current security level

static Set<string> PowerUsers; // Level 1 people (initialized elsewhere)

static Set<string> NormalUsers;// Normal users (initialized elsewhere)

// Rule for successful login at security level 1

[Rule(Action="Login(userId, 1) / true")]

static void LoginLevel1Worked(string userId)

{

Condition.IsTrue(PowerUsers.Contains(userId)); //Unknown-step fails

userName="P."+userId; // Step possible; add Power User Prefix

securityRing=1; // Assumed due to Action label

loggedIn=true; // Already know this login is good

// result==true assumed due to Action label

}

// Rule for failed login at security Level 1

[Rule(Action="Login(string userId, 1)/ false")]

static void LoginLevel2Failed(string userId)

{

Condition.IsFalse(PowerUsers.Contains(userId)); //Unknown-step fails

loggedIn=false; // Still in rule; so assumed due to Action label

securityRing=0; // Logged out default state values

userName="";

// result==false assumed due to Action label

}

// Rule for login attempt at any level except security level 1

[Rule(Action="Login(userId, securityCode) / result")]

static bool LoginNotLevel1(string userId, int securityCode)

{

Condition.IsTrue(securityCode > 1); // Rule only for legal non-level 1

if (NormalUsers.Contains(userId)) // Step OK; check if user known

{

userName="U."+userId; // User known, so login succeeds

securityRing=securityCode;

loggedIn=true;

}

else // User unknown, so login fails

{

loggedIn=false;

securityRing=0;

userName="";

}

return loggedIn; // result == returned value

}

Rob DuWors

Spec Explorer 2010, Release 3.2 Now Available!

2010-04-20T00:08:27Z

Spec Explorer 2010 Release 3.2

Hello! We are delighted to announce the newest version of Spec Explorer 2010, Release 3.2.

Spec Explorer 2010 Release 3.2 contains new and enhanced features, improved documentation, plus over 110 bug fixes. It runs on the Visual Studio 2010 Professional level product and above.

What’s New in Spec Explorer?

This release also contains new features including:

New Model Wizard: The new Model Wizard conveniently consolidates solution and project creation by unifying the previously separate Spec Explorer Model Project and Spec Explorer Base Solution templates.
Choice API: The new Choice feature has been added to assist support where the System Under Test may provide one of several compliant responses to a single action. While Spec Explorer previously supported such non-determinism the new feature makes it simpler to model.
SpecExplorer.exe: The automation version of Spec Explorer has been updated to support the newest standard format for exploration results and to provide better automation support for custom-written post processor extensions.
Improved Documentation: While continuing to improve the overall quality of the Spec Explorer documentation the description of the Cord Scripting Language has been extensively revised in particular, and every page of the documentation now has a version header to clearly indicate the version of Spec Explorer that the documentation describes.

Where can you get it?

The Spec Explorer downloads can be found on the Spec Explorer home page on DevLabs.
See the on-line Release Notes for the latest, more detailed description of installation requirements, major features, bug fixes and known issues. Further information can also be found on The Spec Explorer Forum, The Spec Explorer Team Blog, and the latest Spec Explorer Help Documentation is always available in the MSDN library.
Please note that Spec Explorer 2010 Release 3.2 now runs only on the released version of Visual Studio 2010. It does not work with Beta 1 or 2 or the Release Candidate versions of Visual Studio 2010, nor with Visual Studio 2008. The 90 day trial version of Visual Studio 2010 can be found at here.

We hope you enjoy this release and look forward to hearing feedback from the Spec Explorer community.

The Spec Explorer Team

Effective Model-Based Testing with Spec Explorer Full Class

2010-03-31T18:51:50Z

The full video series for the modeling class is available on Channel 9! It’s the recording of a two-half-day course Wolfgang and I gave on the Microsoft Redmond campus.

The training is long (about 8 hours), but we have split it for your viewing convenience into 4 lectures (sessions). Each session has in turn 4 parts.

Enjoy!

Caveat: The quality of the screen captures makes them hard to read. These videos will be replaced with new ones recorded with a better quality in the future. Please, forgive any inconvenience this might cause you.

Announcing Spec Explorer 2010, Release 3.1!

2010-02-16T05:38:00Z

Spec Explorer 2010 Release 3.1

Note: Now obsolete. Please use Release 3.2.

Greetings! Today we are proud to announce of the newest version of Spec Explorer 2010, Release 3.1.

Running only on Visual Studio 2010 Release Candidate (RC), Spec Explorer 2010 Release 3.1 contains major enhancements, new features, and over 220 bug fixes.

What’s New in Spec Explorer?

Please note that core modeling attributes and classes have been renamed and revised to make them more consistent and clear. Spec Explorer users should be aware that the continued use of these deprecated items in this release will generate warning messages. Usage of the new attributes and classes is highly encouraged, as is migration of prior models and scripts from the older usage.

This release also contains significant new features including:

· Flexible test naming and attributes: New and revised switches allow finer control over test case naming and attributes including the ability to construct switch values using system environment variables and newly provided Spec Explorer built-in variables.

· Bounded repetition machine: Cord now supports additional ways to specify a repeating behavior for a specific number of times or a range of repetitions.

· New project creation: The Spec Explorer model project template can now be used to create a new project within an existing or a new solution whereas only solutions could be created before.

· Construct tag and switch completion: Cord now supports automatic completion of tags in the Construct statement and for switch names.

· F1 help: the built-in Help Viewer of Visual Studio 2010 will display top level information for each type of window in Spec Explorer using the F1 key.

· Help integration: Spec Explorer documentation is now fully integrated with the Help Manager to support both online MSDN Library viewing of help information and locally stored help content. The Help Manager can also be used to update the local copy of help documentation.

· Exploration progress: Spec Explorer provides updated status to give a better indication of the progress being made during lengthy explorations and related algorithms.

· User-customized post processing: User-defined post-exploration processing task can now be launched from within Visual Studio to generate additional artifacts.

Where can you get it?

· The Spec Explorer downloads can be found on the Spec Explorer home page on DevLabs

· See the on-line Release Notes for the latest, more detailed description of installation requirements, major features, bug fixes and known issues

· Further information can also be found on The Spec Explorer Forum, The Spec Explorer Team Blog, and the latest Spec Explorer Help Documentation is always available for the MSDN library.

We hope you enjoy this release,
The Spec Explorer Team

Spec Explorer Webcast in German Online

2010-02-02T18:27:35Z

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

2010-01-31T15:22:49Z

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

2009-11-24T22:08:48Z

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);
}

Notes on this code:

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

2009-11-24T00:39:36Z

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

2009-11-24T00:36:59Z

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

2009-10-28T16:56:03Z

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?

2009-10-27T20:35:56Z

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!

2009-10-27T12:20:00Z

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.

Beijing Spec Explorer Team	Redmond Spec Explorer Team

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.