Model Based Testing using Spec Explorer

Model Based Testing or simply MBT relies on Behavioral Model of an implementation names SUT or System Under Test. This is why a model needs to be more abstract than the SUT itself and this can be achieved by encapsulation or by overlooking the details. The behavioral pattern can be achieved by monitoring the SUT’s runtime behavior. Let us illustrate the Model Based Testing in Detail using the Spec Explorer for Visual Studio 2010.

Model Program is the testing model based on the behavioral pattern of SUT. The model program consists of a Cord Script, where the configurations and machines defining the exploration are being defined. Then, we need a model program where the system behavior is being defined. In the following Cord Script, we can see that, we have two implementations Add and ReadAndReset and so we have declared two actions into config Main.

ParameterCombination has been used to test the implementations with given parameter range or constraint. We have to create the machine where, model program defines the state variables and update rules of an abstract state machine. The state of a machine captures a snapshot of variable values in each step where it satisfies the state based pre-conditions. It then explores the machine’s state and transitions which results a finite graph which is eventually the subset of Model State and Transitions. So, the actions of implementations are being defined in the Cord Script whereas the Rules that model the action described in Cord script into the Model Program. And, Model automation can be enhanced by different scenarios of behavioral pattern of the program.

(a) Cord Script: This is a Spec Explorer coordination script where we define configurations and machines describing the exploration to be performed.

using MyMBTSample.Sample;

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

config Main

{

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

action abstract static void MyMBT.Add(int x);

action abstract static int MyMBT.ReadAndReset();

switch StepBound = 128;

switch PathDepthBound = 128;

switch TestClassBase = "vs";

switch GeneratedTestPath = "..\\MyMBTSample.TestSuite";

switch GeneratedTestNamespace = "MyMBTSample.TestSuite";

switch TestEnabled = false;

switch ForExploration = false;

}

/// This configuration provides a domain for parameter in the previous one.

config ParameterCombination: Main

{

action abstract static void MyMBT.Add(int x)

where x in {0..2};

}

/// Constructs a machine from the model program. Since the model is not finite, this machine explodes and exploration is stopped by a bound. Switch For Exploration makes the machine appear in Exploration Manager.

machine MyMBTModelProgram() : Main where ForExploration = true

{

construct model program from ParameterCombination

where scope = "MyMBTSample.MyMBTModelProgram" //The value of the namespace switch can be a .Net namespace or a fully-qualified class name.

}

/// Defines a scenario for slicing. When explored on its own, this machine leaves all its parameters unexpanded.

machine DoubleAddScenario() : Main where ForExploration = true

{

//Omitting the parenthesis for an action invocation is equivalent to setting all its parameters to _ (unknown).

(Add(_); Add; ReadAndReset)*

}

/// selects the slice of the model program that matches the scenario. The model program supplies all parameter and state data omitted from the scenario.

machine SlicedMyMBTModelProgram() : Main where ForExploration = true

{

DoubleAddScenario MyMBTModelProgram // (synchronized) parallel composition

}

/// Builds a machine resulting from a link coverage traversal of the sliced model program. It can be explored or saved as a C# test suite that can be run in a VSTS unit test project (by pushing the Generate Test Code button in the Exploration Manager toolbar). Most tests should fail, since the sample implementation is empty.

machine MyMBTTestSuite() : Main where ForExploration = true, TestEnabled = true

{

construct test cases where strategy = "ShortTests" for SlicedMyMBTModelProgram()

}

(b) Model Program:

using System;

using System.Collections.Generic;

using System.Text;

using System.Linq;

using Microsoft.Modeling;

namespace MyMBTSample

{

/// <summary>

/// An example model program.

/// </summary>

static class MyMBTModelProgram

{

static int MyMBT;

/// <summary>

/// A rule that models the action of incrementing

/// the MyMBT by a number.

/// </summary>

/// <param name="x">The increment to be added to the MyMBT.</param>

[Rule(Action = "Add(x)")]

static void AddRule(int x)

{

Condition.IsTrue(x > 0);

MyMBT += x;

}

/// <summary>

/// A rule that models the action of reading the

/// current value of the MyMBT and then setting

/// it back to zero.

/// </summary>

/// <returns>The value of the MyMBT before being reset.</returns>

[Rule(Action = "ReadAndReset()/result")]

static int ReadAndResetRule()

{

Condition.IsTrue(MyMBT > 0);

int oldValue = MyMBT;

MyMBT = 0;

return oldValue;

}

}

}

Now, if we want to explore the Models in Graphical representation, we get the following:

MyMBTModelProgram():

DoubleAddScenario():

SlicedMyMBTModelProgram() :

MyMBTTestSuite():

- Test Suite: Model based test are being generated in two ways of which one is Offline testing or tests are being generated from a given specification or model and another way is named as Online or On-the-Fly where tests are being generated while the testing progresses. Tests may include the aspects of expected behavior or expected results or may be to run the SUT for validation.

namespace MyMBTSample.TestSuite

{
using System;
using System.Collections.Generic;
using System.Text;
using System.Reflection;
using Microsoft.SpecExplorer.Runtime.Testing;
using Microsoft.VisualStudio.TestTools.UnitTesting;


[System.CodeDom.Compiler.GeneratedCodeAttribute("Spec Explorer", "3.4.2965.0")]
[Microsoft.VisualStudio.TestTools.UnitTesting.TestClassAttribute()]
public partial class MyMBTTestSuite : VsTestClassBase {

public MyMBTTestSuite() {
this.SetSwitch("ProceedControlTimeout", "100");
this.SetSwitch("QuiescenceTimeout", "30000");
}

#region Test Initialization and Cleanup
[Microsoft.VisualStudio.TestTools.UnitTesting.TestInitializeAttribute()]
public virtual void TestInitialize() {
this.InitializeTestManager();
}

[Microsoft.VisualStudio.TestTools.UnitTesting.TestCleanupAttribute()]
public virtual void TestCleanup() {
this.CleanupTestManager();
}