Model Programs
A model program is a set of rules written in a programming language, such as C#, that enables the expression of both interaction-oriented and state-oriented modeling styles. In this documentation, the terms model program and rule program are synonymous.
In Spec Explorer, the modeling effort involves writing a model program class containing modeling methods that model the behavior of interest in the system under test (SUT). These modeling methods often correspond to methods in the SUT implementation. Model program methods are decorated with attributes to designate them as part of the model in various ways, for example, as rule methods. The model program is joined by a Cord script that defines configurations and action machines expressing behaviors that further constrain the model for purposes of generating practical test cases. The buildup to a final testable model is coded in the Cord script, typically as the culmination of a series of explored action machines. A model program can be written manually or derived from existing code. It must express all legal sequences of actions or behaviors--the greatest superset of potential behaviors--that then must usually be pared down in the Cord script to be testable. For techniques used to perform this practical paring down, see Scenarios and Slicing.
A model program consists of the following:
Methods that model behavior of interest in the SUT
Rule and other model program attributes
Rule logic expressed using Spec Explorer's Modeling Support API
Data about model state
Relationship between Model Program and Cord Scripting
The Cord script can be thought of as completing the model that is initially expressed in the model program. The Model program and the Cord Script work in tandem to make a testable model of the SUT. Most of the expressive power needed to culminate in a testable model is provided by Cord scripting.
A Cord script must never be used to restrict illegal actions permitted in the model program.
The Cord script should have the maximum possible number of exploration directives and restricted action sequences, or scenarios.
Relationship between Model Program and Test Suite
The relationship between model and test suites is lightweight. The model is used to generate traces, which are used both as input test sequences and as the output oracle to determine whether the system behaves correctly. The resulting testing approach is "black box" in two senses: it has no access to the internal states of the implementation, and it does not store model states in any way. Thus the model does not need to be distributed with the test suite, which is stand-alone.
With Visual Studio, the model program is not accessible from the test suite.
The only information from the original model that is incorporated into the generated C# test cases is the action sequences (or steps) and their associated parameter values, both input control and output oracle.
See Also
Concepts
Modeling
Test Generation
Rule Attribute