Models
As a model-based testing (MBT) tool, Spec Explorer leverages models of the system under test (SUT). In general, such models have the following essential characteristics:
Models represent an abstraction of a system from a particular perspective.
Models support investigation, construction, and prediction of the modeled system.
Models are described in many ways, depending on the discipline. They can be described by use of diagrams, tables, text, or other kinds of notations. They might be expressed in a mathematical formalism or informally, where the meaning is derived by convention.
Although computing equipment and software plays an important role for the application of modeling in science and engineering, modeling is not as ubiquitous in software engineering as it is in other engineering disciplines. However, formal methods is one discipline where modeling has been applied in the areas of safety- and security-critical software systems. Diagrammatic models, such as state charts, have been used in the embedded systems area. Unified Modeling Language (UML) and Domain Specific Languages (DSL) are being increasingly used in association with model-driven development (MDD) and model-driven architecture (MDA).
The effort to model a system incurs an initial cost that yields a return on the investment because of the inherent leverage afforded by abstraction. Here is a breakdown of that return on investment in terms of the main benefits of modeling, especially when the modeling process itself is software-assisted.
The process of designing a model provides insights because it requires rigorous thinking about the system in terms of actions, states, and steps.
Animation makes the behavior of the modeled system visible, often via a graph representation. Such visibility offers feedback that is usually not obvious from the definition of the model alone. Animation informally ensures that the model conveys the intended behavior of the modeled system.
Model checking ensures formally and systematically that the model conveys the intended behavior by verifying that expected properties and requirements hold in the modeled system.
Exploration, an integration of animation and model checking, provides a unified way to validate, analyze, and visualize the model. The model more easily becomes the object of an automated modeling tool in which a logic of explicit constraints can be applied to the potentially infinite domain of the model.
Model-based testing (MBT) more easily reveals whether an implementation conforms to a given model. While MBT cannot formally prove that a model and implementation coincide, it can provide essential confidence that they do. Moreover, if a conformance failure is detected, MBT gives feedback about both the implementation and the model. The model itself might be erroneous.
Test generation can be more easily automated from an explicitly formal description of the model. With a model expressed in software it is easier to change the model and then automatically regenerate a corresponding new suite of test cases.
Software Models
There are two fundamentally different kinds of software models: structural and behavioral.
A structure model describes the entities that make up the architecture or design of a software system and the static relationships between them. These entities can include processes, components, and classes. A typical example of a structure model is a class diagram.
A behavior model describes how software systems react when provided with certain inputs. A behavior model can also describe how software systems react after time lapses, which can be regarded as a special kind of input. Reaction is thereby defined by the outputs the system produces. A state machine is an example of a typical behavior model.
When models are mentioned in the context of model-driven development/architecture, the implicit reference is to structure models. Notations and tools for structure models are well supported as part of mainstream IDEs like Visual Studio. Behavior models are the software models exploited by Spec Explorer and are the main focus in this documentation.
Behavior models can be expressed in many different styles and notations. In terms of style, there are two important families: interaction-oriented and state-oriented.
In an interaction-oriented modeling style, input-output behavior is described from the viewpoint of an outside observer who sees interactions of system components. Typical instances of interaction-based model notations are use cases and sequence diagrams.
In a state-oriented modeling style, input-output behavior is specified from the viewpoint of describing the system states. For each state, possible transitions to other states and the actions that trigger them are described. A typical instance of state-based model notations are state machines in any of their various forms, such as state charts, extended finite state machines, or abstract state machines.
Models can have diagrammatic or programmatic (textual) notations. Both styles can be expressed in both of these kinds of notations.
Spec Explorer Models
In general, Spec Explorer's powerful architecture is designed to support all combinations of styles and notations. Models in Spec Explorer start with a notation called model programs. Model programs are written in a programming language, such as C#, and allow expression of both interaction- and state-oriented modeling styles. Spec Explorer is an MBT tool that uses state-oriented model programs that are coded in C#. A Spec Explorer model consists of a set of rules expressed in a model program combined with behavioral descriptions coded in a powerful scripting language called Cord. The model program and the Cord script work together to make a testable model of the SUT. Most of the expressive power needed to culminate in a testable model is provided by the Cord script. The Cord script may be thought of as using the model program to achieve a testable model. For more information about model programs, see Model Programs.
For more details on using models in Spec Explorer, see Modeling.