State Checker Pattern

When creating a model for a system, the model is an abstraction in which one state corresponds to several states in the system. For example, the model can ignore cache that the system uses to improve performance and also to combine states with different cache contents. Ideally, the test cases generated for a model validate that the system is always in the state predicted by the model at that point in the test.

Problem

Spec Explorer uses model states only to evaluate enabling conditions and parameter values of rules. Rules, in turn, can update model state, but this influences only which rules are enabled in the new state and the parameter values that should be passed. Model states are not included in generated test code; only action labels resulting from rules being explored are included. Therefore, test cases have no access to model state, but only to the actions (and their arguments) predicted by the model.

However, test cases only call methods on a system under test and expect events to be raised by that system based on the rule labels in the model exploration steps. Because test cases are generated from a model, they are composed of operations declared as rules in the model configuration. They do not have access to the state of the system under test.

This section provides a pattern to validate that the system is in the correct state with respect to the model state. This can be done despite the fact that the model state is visible only through action arguments, and the system state is not directly accessible to the test case.

Forces

The solution to this problem requires synergy between the model and the adapter or harness that connects test cases to the system under test. The solution must take into account the competing forces of keeping the model simple, not overstretching the role of the harness, and generating non-intrusive test suites.

Test cases are usually not generated from the raw model, but rather from the result of applying traversals to it. Models often have loops that could result in never-ending test cases, and controllable choices that can be eliminated before testing. The purpose of traversals is to select certain paths of the model that are suitable to be turned into test cases. Even if check actions are enabled in all relevant model states, there is a chance that a traversal might reduce the number, based on the coverage criteria, but still cover each step at least once.

Solution

Spec Explorer provides state-checker actions that can be called in all model states for which the system is to be validated: void stimulus (call-return).

This action only sends information from generated test cases to the harness. There is no response or result coming from the system under test that the test case can check.

The pattern works by performing the actual check in the harness. State-checker actions are only a means to convey to the adapter the information about the model state needed to verify the current system state.

State-checker actions consequently have parameters representing all aspects of a model state needed to check the correctness of corresponding system states. Preconditions in the model program ensure that these parameters have the correct value for each state.

In exploration, state checkers result in self loops; that is, the source state for the call is the same as the target state for the return. There is no change to any state variables. There is no concept in the model of a state checker failing, because all state-checker methods are of type void and state-checker methods do not change state variables. The success or failure of a state checker is resolved within the harness or adapter after accessing the system state. The test must fail if the system under test is not in the correct state, according to the data received from the model through state-checker actions.

Example

This example is based on extending the template solution generated by the Modeling Wizard. That solution is called the static model template. To generate an instance of the static model template code as a starting point for this example, see Creating the Solution; to generate the static model template as part of the entire first-time tour, see Using Spec Explorer for the First Time. Note that for purposes of exposition, the code exhibited in this example is extracted from the static model template and may be missing some of the other static model template code that is not relevant to the explanation here. Note also that this example assumes that the static model template's projects are used, which determines relevant namespace dependencies and the location where test code is generated.

In this example, a model state is represented by model variable accumulator. Test cases generated from this model verify that the implementation maintains the right value when the ReadAndReset action is called. Although the action is enabled in all states, generated test cases call it only occasionally, because it also changes the value of the counter.

Test cases generated from the model contained in the static model template fail only when the final call to ReadAndReset does. In fact, although the implementation included with static model template has no accumulator, which prevents it from correctly performing an Add operation, only some test cases fail: those that return a final result other than 4.

If a user wants to make sure that the value for accumulator, or its equivalent, maintained by the system under test matches the model prediction in every state, the user would apply this modeling pattern by extending the configuration in the Config.cord script with a state-checker action, as shown in the following Cord code example.

config Main
{
   action abstract static void Accumulator.Add(int x);
   action abstract static int Accumulator.ReadAndReset();
   action abstract static void Accumulator.Checker(int accumulatorState);

   // ... switch values ...
}

The model program in the AccumulatorModelProgram.cs file must also be extended with a rule method enabling the checker in all model states. Its only precondition forces the parameter to contain the value of model variable accumulator.

The following code example shows how to extend the AccumulatorModelProgram class by adding the Checker rule method.

static class AccumulatorModelProgram
{
   static int accumulator;

   [Rule(Action = "Add(x)")]
   static void AddRule(int x)
   {
      Condition.IsTrue(x > 0);
      accumulator += x;
   }

   [Rule(Action = "ReadAndReset()/result")]
   static int ReadAndResetRule()
   {
      Condition.IsTrue(accumulator > 0);
      int oldValue = accumulator;
      accumulator = 0;
      return oldValue;
   }

   [Rule]
   static void Checker(int accumulatorState)
   {
      Condition.IsTrue(accumulatorState == accumulator);
   }
}

This precondition effectively makes the model state variable accumulator available in the Checker rule. In Exploration Manager, an exploration of the AccumulatorModelProgram machine shows a self loop labeled with the Checker rule for every state, and the value of the accumulator in that state as an argument. The following illustration shows a fragment of the exploration graph.

As indicated in the graph, the exploration hits the step bounds. For a model with a finite state space, test cases would be generated directly from this machine, without needing further adjustment. However, since the test space of this sample model is infinite, it must be sliced in the Cord script before generating tests. The static model template provides a DoubleAddScenario (in file Config.cord) that achieves this slicing as shown in the following code example.

machine DoubleAddScenario() : Main where ForExploration = true
{
   (Add(_); Add; ReadAndReset())*
}

When composed with the model program, this scenario cannot be used as is for the State Checker pattern, because it would remove all occurrences of the Checker rule. Therefore, an extended new scenario is needed to insert a loop (zero or more Checker invocations) between each pair of consecutive invocations. This can be done by adding a scenario with a composition using the Interleaved ParallelBehavior operator (|||), as shown in the following Cord code example.

machine ScenarioWithCheckers() : Main where ForExploration = true
{
   (Add; Add; ReadAndReset)* ||| Checker*
}

After adding this code to the Config.cord file and exploring this machine by itself, the following graph results.

Checker is invoked in all scenario states. The scenario does not provide parameter values. It must be composed with a model program to get concrete arguments for all actions. This is shown in the CheckedModel machine in the following Cord code example.

machine CheckedModel() : Main where ForExploration = true
{
    ScenarioWithCheckers || AccumulatorModelProgram
}

The exploration graph for the CheckedModel machine has the expected checker loops, as shown in the following exploration graph.

The arguments for these steps are forced by the model to be the actual values of the accumulator in each state. For example, in state S13, value 1 and value 2 have been added, and thus the checked accumulator value exposed by the checker is 3.

To generate tests from this model, the following test suite scenario code (based on the sliced and checked version of the model) is added to the Config.cord file.

machine TestSuiteWithCheckers() : Main where ForExploration = true, TestEnabled = true
{
   construct test cases for CheckedModel
}

The TestCasesConstruct behavior is used to define this test suite scenario. Spec Explorer ensures that self loops are explored once every time a state is hit. The following illustration is the exploration graph for the TestSuiteWithCheckers machine.

Test cases generated from this machine invoke the checker on the harness at every step, and pass the checker the expected value for accumulator. The harness then obtains an accumulator value from the implementation to ensure that the value matches that received from the model. If the value does not, the test case fails.

Note that in using the static model template, the test cases generated from this new TestSuiteWithCheckers machine are written to the folder location of the SpecExplorer1.TestSuite project in file TestSuiteWithCheckers.cs. However, this file is not automatically added to the Visual Studio project. You do this manually by right-clicking on the project and choosing Add\Existing Item.... This addition is required in order to later run the tests.

In this example, there is no separate adapter or harness, so this task must be performed by the implementation itself. Because it maintains no accumulator variable, one must be added. However, the Add method is not fixed, so the counter never changes its value, and all tests fail, not just those that have a final result other than 4.

The other change in the implementation is the introduction of the Checker method, needed for the test to run. If the current value of the implementation accumulator does not match that received from the model, the test suite must fail. To run the test successfully, this example uses the equality Assert available in Visual Studio Test Tools. Note that to use the Assert, the VisualStudio.TestTools namespace needs to be available. However, the SpecExplorer1.Sample project, as generated by the Model Wizard, does not include an assembly reference to provide that namespace. To add the assembly reference to the project, you can get the full reference path to that assembly (Microsoft.VisualStudio.QualityTools.UnitTestFramework.dll) by looking in the References for the SpecExplorer1.TestSuite project. The static model template provides an implementation project, SpecExplorer1.Sample, with an Accumulator class to which the needed Checker method can be added, as shown in the following code example.

public class Accumulator
{
   public static void Add(int i)
   {
   }

   public static int ReadAndReset()
   {
      return 4;
   }

   static int myAccumulator = 0;

   public static void Checker(int modelAccumulator)
   {
      Microsoft.VisualStudio.TestTools.UnitTesting.Assert.AreEqual
            (modelAccumulator, myAccumulator, "Accumulator mismatch: Model vs Implimentation.");
   }
}

The generated tests are run by choosing Run\All Tests in Solution from the Visual Studio Test menu. When run against this checked implementation, all test cases in the new test suite fail as soon as they check the state. The following illustration shows the test results.

The following shows the log entry for the first TestSuiteWithCheckers failed test.

Error message:
Assert.AreEqual failed. Expected:<1>. Actual:<0>. Accumulator Mismatch: Model vs Implementation

Standard Console Output:
Beging executing test TestSuiteWithCheckersS4
reaching state 'S4'
executing step 'call Checker(0)'
reaching state 'S5'
checking step 'return Checker'
reaching state 'S10'
executing step 'call Add(1)'
reaching state 'S14'
checking step 'return Add'
reaching state 'S18'
executing step 'call Checker(1)'

Variants

In the example toured above, a trace-selection scenario must be expanded to include checkers. This is not necessarily the case for all models. More loose scenarios that use the universal behavior represented by an ellipse (...) or generic steps, represented by an underscore (_), would automatically include them.

The operator used for the expansion was the Interleaved ParallelBehavior operator (|||). Alternatively, the Synchronized-interleaved ParallelBehavior operator (|?|) could be used in the composition. That would require defining a Checker action in a separate configuration, as in the following code example.

config NoCheckers
{
   action abstract static void Accumulator.Add(int x);
   action abstract static int Accumulator.ReadAndReset();
}
config Checker
{
   action abstract static void Accumulator.Checker(int accumulatorState);
}
config Main: Checker, NoCheckers
{
   switch StateBound = 128;
   switch StepBound = 128;
}
machine ScenarioWithoutCheckers() : NoCheckers
{
   (Add(_); Add(_); ReadAndReset())*
}
machine CheckerScenario() : Checker
{
   Checker*
}
machine ScenarioWithAddedCheckers() : Main
{
   ScenarioWithoutCheckers |?| CheckerScenario
}

A different approach would be to use one of these operators to compose two model scenarios: one without checkers (as in the DoubleAddScenario machine in the original state checker approach above), and another one sliced to contain the checkers only, as shown in the following code example.

machine AnotherCheckedModelProgram() : Main
{
   DoubleAddScenario ||| ( Checker* || AccumulatorModelProgram )
}

All these alternatives are equivalent.

Results

The State Checker pattern has the following benefits:

• Users can write code to check system states during test execution.

• Checker methods can obtain information that was originally in the model passed on through expected actions and their arguments.

• The Spec Explorer traversal algorithms guarantee that the checks are performed every time a state in which they are enabled is traversed in a test case.

This pattern has the following limitations:

• Although checkers are represented as rules in the model, there is no associated model logic. The model is not aware of the validation logic.

• The harness or adapter does all validation. This increases the coupling between model and harness.

• Checker actions clutter exploration graphs without helping the user to understand the behavior.

• There might be actions that result in self loops, but these actions are not supposed to be state checkers. There is no mechanism to distinguish such actions from checkers. Spec Explorer expands self loops in all test cases, including their associated states, as it does with state checkers.

• State checkers must be enabled in any scenarios used for slicing. Otherwise, they do not appear in test cases that result from that slicing.

See Also

Concepts

Creating the Solution
Using Spec Explorer for the First Time

Other Resources

Modeling Toolbox