A Model Program is an executable specification for another program or system, called the implementation. Usually the model program is much smaller and simpler than the implementation. The model program can be analyzed to check for design errors in the implementation, can generate test cases for the implementation, and can serve as the oracle that provides the correct results when testing the implementation.

In NModel, model programs are used in two ways. A contract model program represents all of the allowed behaviors (runs or traces) of the implementation, while a scenario model program represents a collection of runs (perhaps just one) that are related in some way: a test suite, or a temporal property to check during analysis.

NModel currently supports two languages for writing model programs: C#, and a term representation for Finite State Machines (FSMs). Contract model programs are usually written in C#, while scenario model programs are usually expressed as FSMs.

A C# model program uses attributes and data types from the NModel library. It uses the NModel namespaces and references NModel.dll. It must use the library data types for collections and objects, not the usual C# and .NET data types.

A C# model program is defined by the contents of a single namespace, whose name is the model program name. The state (stored information) of a model program is stored in state variables, the static fields and instance fields declared in its namespace. The actions (state transitions) of the model program are the static methods and instance methods in its namespace that are labeled with the [Action] attribute. The control structures of a model program are its enabling conditions, Boolean methods that are true in states where an action can occur. A C# model program can also have a factory method that prepares the model program for use by the NModel tools (in recent NModel releases, a factory method is not necessary).

A C# model program can be built up from separate features, classes identified by the [Feature] attribute, which can be optionally included or excluded from the model program.

Separate model programs can be combined by composition. When programs are composed, shared actions synchronize and unshared actions interleave. Compose a contract model program with a scenario to achieve scenario control for testing, or to check a temporal property during analysis. Compose two or more contract model programs to build up complex models in a well-structured way.

Here is a C# model program named PowerSwitch with one state variable power that can take on the two values On and Off, two actions PowerOn and PowerOff, their enabling conditions PowerOnEnabled and PowerOffEnabled, and a factory method Create.

using NModel;
using NModel.Attributes;
using NModel.Execution;

namespace PowerSwitch
{
  enum Power { On, Off };
  public static class Contract
  {
    static Power power = Power.Off;

    [Action]
    static void PowerOn() { power = Power.On; }
    static bool PowerOnEnabled() { return power == Power.Off; }

    [Action]
    static void PowerOff() { power = Power.Off; }
    static bool PowerOffEnabled() { return power == Power.On; }

    public static ModelProgram Create() { return LibraryModelProgram.Create(typeof(Contract)); }
  }
}

It is more usual to express such a simple model program as an FSM, represented by a data structure called a term. Here the first argument of the term is the initial state, the next argument is a list of accepting states where runs are allowed to stop (empty here to indicate runs may stop in any state), and then a list of state transitions. Each state transition is a triple: the current state, the action (transition label), and the next state.

FSM(Off, AcceptingStates(), 
    Transitions(t(Off, PowerOn(), On),  t(On, PowerOff(), Off)))

Both the C# model program and the FSM here exhibit the same behavior: they describe the same runs. In these examples, only one action is enabled in each state. Model programs can exhibit nondeterminism, where more than one action is enabled in some states.

More complex model programs appear in the examples.

The NModel framework provides several command-line programs. To analyze a model program and visualize its behavior, use mpv. To generate test cases, use otg. To execute test cases, or to generate and execute test cases on-the-fly, use ct.

Last edited May 1, 2008 at 1:05 AM by veanesm, version 1

Comments

No comments yet.