Functional Workflow
The following illustration shows a workflow perspective on the functioning of Spec Explorer. The white items represent the main functional parts of Spec Explorer.
.gif "SE Workflow")
The workflow is characterized by a unified approach to exploration and traversal. This enables a consistent usage paradigm, essentially based on an extended notion of exploration.
Inputs
| Input | Description |
|---|---|
A set of .NET model assemblies |
The .NET assemblies are created from a model program in C# or another .NET language. Model source is compiled with a standard compiler. It is usually annotated with custom attributes for marking modeling constructs. Other model notations, such as diagrams, can be incorporated by first translating them into C# or the Cord modeling language. |
A set of .NET harness, or adapter, assemblies |
These can potentially include the implementation under test. If the implementation under test is included, its presence enables the tool to validate consistency of bindings from model to implementation. There is no difference between model assemblies and implementation/harness/adapter assemblies; that is, they all constitute a single set of assemblies referenced by Spec Explorer. |
A set of coordination (Cord) scripts |
These scripts describe action sets, mapping to metadata in provided assemblies, configuration options, and behaviors in the form of action machine definitions. |
An exploration goal |
The user can provide an exploration goal through the user interface (UI) or the command line. An exploration goal identifies the machine to explore and the exploration method to use. |
Tool Functionality
Based on these inputs, the core algorithmic functionality of the tool is the following:
Validating the consistency of the inputs. This means checking whether references in the scripts to elements in the assemblies are resolvable, as well as checking the syntax and context conditions of the script language itself.
Running exploration, as defined by the exploration goal. This means systematically running the goal machine to determine the reachable state space and state transitions.
The goal machine can be specified by the scripts, by a reference to a model program from the assemblies, or by composition or transformation of other machines. Processes traditionally available in model-based testing tools such as traversals are represented as particular transformations on machines, which provide a uniform paradigm for state exploration and traversal.
Outputs
The outputs from running an exploration are presented and processed in the following way:
The state graph that results from exploration. The user can click states and steps in the graph and inspect their content and properties. The display can be configured in various ways in a Cord script.
The graph is also encoded in a data structure called the transition system. This is a programmatic representation with a direct correspondence to an XML format that can be output. Moreover, the transition system can be translated into C# code that runs offline tests.
Because exploration and traversal are unified, the result of exploration—whether displayed as a graph, XML transition system, or C# test suite—can represent various logical artifacts: the explored state space, a test suite, a model-checking counterexample, or the log of a test run.
The output from the On The Fly test system is a series of interactions with the system under test (not shown). Exploration and the On The Fly test system interact with each other, with the On The Fly system querying the Exploration one step at a time to determine what output to send to the system under test. Note that the Exploration in this case does NOT perform a full exploration of the model, and this Exploration is NOT available as a transition system or to the Test Code Generator.