Spec Explorer Glossary
This glossary contains terms relevant to Spec Explorer as well as to model-based testing.
.seexpl file
A compressed set of XML files that together represent the exploration result of an action machine in Spec Explorer. The set of files includes the transition system for the machine.See also: action machine, transition system.
abstract identifier pattern
A design pattern that allows a user to map an abstract identifier (that is, one that is valid only in the model context) to a fixed identifier that is returned by the system under test.
abstract machine
See definition for abstract state machine.abstract state machine
A state machine that operates on states that contain arbitrary data structures, and where state transitions are defined as a set of transition rules that update each state to produce the next state.See also: action machine, state machine.
accepting state
In Spec Explorer, a state that represents a legal termination point of the exploration of an action machine.See also: action machine, exploration, state.
action
In Spec Explorer, an interaction with the system under test as seen from the test system's perspective. An action is declared in a Cord configuration and can be classified as a controllable (input) or observable (output) action. Controllable actions include call actions, and observable actions include event actions and return actions.See also: atomic action, call-return action, Cord script, event action.
action argument
The variables or literals provided for the action parameters in an action invocation. Action invocation arguments, if specified, must always match, in type and position, the signature provided by the action declaration in the applicable Cord configuration.See also: action, action declaration, action invocation.
action declaration
The declaration within a Cord configuration of the name and parameters of an action. The declaration includes whether the action is a call-return or an event action and whether the action is static or instance-based.See also: action, action invocation, action parameter.
action invocation
A reference to a declared action. Action invocations are used in Cord behavior expressions and in Rule attributes.See also: action, action argument, action declaration.
action machine
An abstract state machine where each transition is labeled with an action, which can contain symbolic information. In Spec Explorer, an action machine is part of a model of the system under test (SUT) and is defined in a Cord script. Each transition in the action machine is associated with an action invocation that represents an activity of the system under test.See also: abstract state machine, action, action invocation, state machine.
action parameter
The named parameters of the action in the action declaration.See also: action, action declaration, action invocation.
atomic action
An action that is discrete and indivisible.See also: action.
behavior
In model-based testing, the way that a system reacts under a specific set of conditions or stimuli. In Spec Explorer, defined behavior is composed of actions, and observable behavior is a collection of traces.See also: action, behavior composition, trace.
behavior composition
The use of behavior operators to construct new behavior descriptions from previously defined behavior descriptions or defined actions. Behavior composition is used in Cord script to define action machines. Cord provides a set of operators used to compose machine behavior from configurations and other behaviors. For more information, see Behavior Composition.See also: action machine, behavior.
behavior expression
See definition for behavior composition.behavior model
A model that describes how software systems react when provided with certain inputs (or with the passage of time). Spec Explorer deals exclusively with behavior models.
behavior operator
See definition for behavior composition.behavior signature
The offered and context signatures for a behavior.See also: context signature, offered signature.
behavior transformation
See definition for construct behavior.behavioral coverage
The extent to which a test suite tests all behaviors described by a model.
behavior restriction
See definition for slice.built-in variable
In Spec Explorer, one of the value substitution variables that are available in Cord script. Switches can be configured by using substitution of variable values from Spec Explorer’s built-in variables and from system environment variables. These variable substitutions are specified by bracketing the variable name with $ or % symbols.See also: switch.
call action
See definition for call-return action.call-return action
A pair of atomic actions: a call action and a return action. They represent synchronous blocking operations on the system being modeled. In practice, this means that the system performs the operation before returning control to the caller.See also: action.
composition operator
See definition for behavior composition.configuration
The Cord code block that declares actions and defines a set of switches and parameters to control exploration, presentation of the exploration result, and testing.See also: action, Cord script.
configuration file
See definition for Cord script.configuration signature
The set of actions declared for a configuration block.See also: action, action machine, configuration, context signature, offered signature.
conformance
See definition for conformance testing.conformance error
An observed behavior in the system under test that violates or fails to meet a given requirement.See also: conformance testing.
conformance testing
Certification or validation that a system under test (SUT) adheres to a set of requirements and behaves as expected for given inputs. If the SUT passes conformance tests, the SUT is said be in conformance with the set of requirements against which the SUT was tested.constraint solver
An element of Spec Explorer that examines constraints during exploration to identify which steps are available from the current state.construct behavior
A behavior expression that algorithmically constructs a new behavior from another behavior. Cord provides a set of construct behaviors. Original behaviors are called input behaviors, and the new behavior is called the constructed behavior.context signature
For an action machine, the configuration signature for the configuration on which the action machine is based. For a behavior, the context signature of the machine in which the behavior is declared.See also: configuration signature, offered signature.
controllable action
See definition for action.Cord script
The collection of Cord configuration files for a modeling project. The Cord script can be thought of as making use of a model program to achieve a testable model of the system under test (SUT). A Cord script contains at least one configuration, which declares the actions of the model, as well as some exploration switches. It also defines at least one action machine, which constitutes an exploration target. A Cord script is composed of all of the Cord configuration files in an exploration project.See also: action machine, configuration.
Cord scripting language
A scripting language for the configuration of model exploration and testing, and for the definition of action machines.dead path
A path that ends in a non-accepting state.See also: path.
dynamic test strategy
The strategy used by Spec Explorer during dynamic traversal to perform a test. The test strategy can be customized by the user.dynamic traversal
A Spec Explorer testing mode that allows the use of custom exploration traversal algorithms.See also: on-the-fly testing, test code generation.
embedded code
C# code embedded in a Cord script, using the (. expression .) or {. statement .} syntax.See also: Cord scripting language.
the empty behavior
The behavior that contains no actions.See also: action, behavior.
enabling condition
A condition that must be met in the current state for a rule to produce a step.See also: rule, state, step.
end state
An explored state with no outgoing steps.See also: state, step.
error state
A state whose validity cannot be determined.See also: state.
event action
A single atomic action that represents a response coming from the system being modeled. The response can be autonomous or can correspond to a previously received request.See also: action.
event queue
In the Spec Explorer testing environment, a first-in, first-out (FIFO) queue that stores events emitted by the system under test.See also: event action.
execution variable
See definition for built-in variable.experiment
A single test case in on-the-fly testing.See also: on-the-fly testing.
exploration
In Spec Explorer, the operation of creating a transition system from an action machine.See also: action machine, transition system.
exploration bounds
Bounds on model evaluation and exploration. Such bounds are controlled by switch clauses in the action machine definition or in a configuration on which the machine is based.See also: action machine, configuration, exploration, switch, test run bounds.
exploration cleanup
A process optionally applied after exploration to identify and merge states that are equivalent. Two states are equivalent if their contents are equivalent and all outgoing paths from the states consist of steps with the same labels and equivalent states.See also: exploration, state, step.
exploration graph
A visual representation of the states and steps of a transition system. The exploration graph is displayed as an annotated state graph.See also: state, state graph, step, transition system.
Exploration Graph Viewer
A Visual Studio document viewer for displaying exploration graphs.See also: exploration graph.
Exploration Manager
A Visual Studio tool window, similar to Solution Explorer, that provides support for validating and exploring models, and for performing tests.exploration-enabled
Indicates that an action machine can be explored. A machine is enabled for exploration if its ForExploration switch is set to true.See also: action machine, exploration, switch.
explored state
A state for which Spec Explorer has examined and generated transitions.See also: action machine, exploration, state.
finite state machine
A state machine with a finite number of labeled states. Also known as a finite automaton.See also: state machine.
implementation
See definition for system under test.implementation type
A type used in the system under test. Distinct from a model type. Model types can be bound to implementation types with the TypeBinding attribute.See also: model type.
initial state
A starting state of an action machine.See also: action machine, state.
input behavior
See definition for construct behavior.interaction-oriented modeling style
A modeling style in which input and output behavior is described from the viewpoint of an outside observer who sees interactions of system components.interleaved parallel composition operator
An operator that produces a behavior where all steps of the component behaviors are produced.See also: behavior composition.
loop
A path that begins and ends in the same state.See also: path, state.
- machine
See definition for action machine.
- machine exploration
See definition for exploration.
- MBT
See definition for model-based testing.
- MDA
See definition for model-driven architecture.
MDD
See definition for model-driven development.model
An abstraction that represents a system from a particular perspective and that supports investigation, construction, and prediction of the modeled system. In Spec Explorer, a model is created as a set of action machines and describes the system under test (SUT) with enough detail to test aspects of interest in the SUT.See also: action machine.
model checking
In Spec Explorer, determining whether expected properties and requirements hold in the modeled system. Model checking is a separate process from validation.See also: validation.
- model composition
See definition for behavior composition.
model exploration
See definition for exploration.model program
A partial description of an action machine that describes specific aspects of the system under test (SUT). The model program describes the possible states of the SUT, under which conditions each transition is enabled, and how each transition updates the state of the SUT.See also: action, action machine, rule, system under test.
model slicing
See definition for slice.model type
A type used in the model program. Distinct from an implementation type. Model types can be bound to implementation types with the TypeBinding attribute.See also: implementation type.
model validation
See definition for validation.model-based testing (MBT)
Software testing in which test cases are derived in whole or in part from a model that describes some (usually functional) aspects of the system under test.model-driven architecture (MDA)
A software design approach for the development of software systems that provides a set of guidelines for the structuring of specifications, which are expressed as models.model-driven development (MDD)
A software development methodology that focuses on creating models, or abstractions, that are closer to some particular domain concepts than to computing (or algorithmic) concepts.modeling perspective
The aspect of the system that a model is designed to represent or test.non-accepting end state
A state in an exploration that has not been marked as an accepting state and that has no outgoing steps.See also: accepting state, exploration, state.
non-determinism
Any behavior in which the system under test may have more than one legitimate response. The model can predict all acceptable responses but cannot predict which response will be observed at a particular time. In Spec Explorer, this means that either more than one event can happen or more than one atomic return action can follow an atomic call action.See also: action, atomic action, call-return action, event action.
n-wise combination
A combination of n parameters (out of m parameters for the given action). Used to restrict the combinatorial explosion that occurs when all possible values of all parameters are explored.See also: action, action argument, action parameter, exploration, pairwise combination.
observable action
See definition for action.offered signature
The set of actions derived from the behavior expression.See also: behavior composition, construct behavior.
on-the-fly testing
A method of testing where exploration of a model is tightly coupled with interactions with the system under test. Spec Explorer supports this testing along with test code generation and dynamic traversal.See also: dynamic traversal, test code generation.
oracle
See definition for test oracle.outgoing step
A step whose starting conditions are represented by the given state.See also: state, step.
outgoing transition
See definition for outgoing step.output
In Spec Explorer, the observable behavior of the system under test, which includes event actions and return actions. For return actions, the output includes the return value of the method, as well as the value of out and ref parameters when the method exits.See also: action, call-return action, event action.
pairwise combination
A combination of two parameters (out of m parameters for the given action). Used to restrict the combinatorial explosion that occurs when all possible values of all parameters are explored.See also: action, action argument, action parameter, exploration, n-wise combination.
parallel behavior operator
One of the parallel composition operators.See also: interleaved parallel composition operator, synchronized parallel composition operator, synchronized-interleaved parallel composition operator.
parameter domain
The range of values that a given parameter can take during exploration.See also: action argument, action parameter, parameter generation,.
parameter generation
The process of specifying and determining which values are assigned to parameters during exploration of a model.See also: action argument, action parameter, parameter domain,.
path
A sequence of steps in a transition system.See also: step, transition system.
path coverage
A measure of how many explored paths through the exploration are actively tested.See also: path
path length
The number of steps in the path. Each instance of a repeated step is counted in the path length.See also: path, step.
point and shoot
To limit state explosion in a given exploration by using one machine (the point machine) to reach states with desired parameter values and then switching to a different machine (the shoot machine) to continue and complete exploration.See also: action machine, construct behavior, exploration, parameter domain.
probe
In Spec Explorer, state information that can be accessed when examining the transition system generated from an action machine.See also: action machine, state, transition system.
pruning
The removal of paths from a behavior or transition system, based on specific criteria.See also: transition system.
quiescence
During testing, the period of time during which the system under test (SUT) does not produce output but for which the test oracle expects that the SUT could produce output.See also: action, system under test, test oracle.
response
Output from the system under test, which is typically associated with a given stimulus.See also: action, stimulus.
return action
See definition for call-return action.rule
Determines the steps that can be taken from the current state in the model program. In Spec Explorer, rules are represented by methods in the model program that have been marked with the Rule attribute. The Rule attribute has an optional Action argument that specifies an action invocation associated with the rule.See also: action invocation, model program, state, step.
rule machine
An action machine based on a model program. Use the ModelProgramConstruct in Cord to define a rule machine.See also: Cord machine, model program.
scenario
A behavior description in Cord that can be composed with a model program to provide a way to limit (or slice) a model program's general behavior to make the model program more testable.See also: behavior, model program, slice.
scope
In a configuration, a switch on the model program construct that indicates which namespaces contain model program elements.See also: model program, switch.
self-loop
A path that contains a single step that begins and ends in the same state.See also: path, state, step.
sequencing behavior operator
An operator that produces a behavior where the first component behavior precedes the second component behavior. With the tight sequencing operator, the first component behavior is immediately followed by the second component behavior. With the loose sequencing operator, any number of arbitrary actions can occur between the two component behaviors.See also: action, behavior, behavior composition.
slice
To use a scenario and the parallel composition operator to limit another behavior. The limited behavior is called a slice.See also: behavior, behavior composition, scenario.
state
A unique configuration in a state machine that represents a point in a machine's behavior and that uniquely determines which transitions are valid from then on.See also: behavior, state machine, step.
State Browser
A Visual Studio tool window associated with Exploration Graph Viewer that displays the content of a state in an exploration graph or compares the contents of two states in an exploration graph.See also: exploration graph, state, transition system.
state checker pattern
A design pattern that allows a user to write code to check system states during test execution. The test oracle examines behavior, and this pattern allows the model to include a behavior that exposes the model state.See also: behavior, model, state, test oracle.
state explosion
The tendency of an exploration to generate a very large (or infinite) set of states.See also: exploration, state.
state filter
A Boolean condition that indicates whether Spec Explorer includes or excludes a given state from exploration. When the StateFilter attribute is applied to a method, property, or field, Spec Explorer treats the member as a state filter.See also: exploration, state.
state graph
A directed graph whose nodes correspond to internal states of a sequential state machine and whose edges correspond to transitions among these states.See also: exploration graph, state machine.
state machine
A behavior model composed of a defined set of states, a defined set of inputs, and a set of transitions between the states based on the inputs. State machines can also include a set of outputs that the state machine can generate.See also: abstract state machine, action machine, finite state machine.
state space
The set of all possible states of an action machine or abstract state machine, based on the state variables defined for the machine.See also: abstract state machine, action machine.
state transition
See definition for step.state-oriented modeling style
A modeling style in which input and output behavior is described from the viewpoint of describing the system states.step
A transition in the execution in the model. Each step is labeled with an action invocation, which implies an event or a method call or return in the system under test.See also: action declaration, action invocation, model, system under test.
Step Browser
A Visual Studio tool window associated with Exploration Graph Viewer that displays the details of a step in an exploration graph or compares the details of two steps in an exploration graph.See also: Exploration Graph Viewer, step.
step label
An action invocation that relates a step in the model to its corresponding event or method call or return in the system under test.See also: action invocation, model, step, system under test.
stimulus
Input to the system under test. Typically associated with an expected response.structure model
A model that describes the processes, components, classes, and so on that make up the architecture or design of a software artifact and the static relationships between them.sub-behavior
A subexpression of a behavior expression.See also: behavior composition.
SUT
See definition for system under test.switch
A configuration setting within a Cord script. Switches offer a generic way to configure various aspects of tool operation.See also: configuration, Cord script, Cord scripting language.
symbolic exploration
Model exploration where parameters are not given fixed values but remain unassigned symbols.See also: exploration.
synchronized parallel composition operator
An operator that produces a behavior where all steps of the component behaviors must be synchronized and where steps that cannot be synchronized are excluded from the result.See also: behavior composition.
synchronized-interleaved parallel composition operator
A hybrid of the synchronized and interleaved parallel composition operators. This operator produces a behavior where actions in the intersection of the offered signatures of the composed behaviors must synchronize while the remaining actions are interleaved.See also: behavior composition, interleaved parallel composition operator, synchronized parallel composition operator.
system under test (SUT)
Software that is being tested for correct operation, sometimes referred to simply as the system.test case
An executable test. In Spec Explorer, an individual test case is part of a test suite, which is generated from a model.See also: action machine, test suite.
test code generation
The automatic code generation for a test suite. Spec Explorer can create a test suite from a model, and each test case in the test suite can be run against the system under test without further involvement from Spec Explorer.See also: action machine, dynamic traversal, on-the-fly testing, test suite.
test oracle
A collection of traces, where each trace describes a compliant behavior of the system under test. Spec Explorer can use a transition system as a test oracle and can use the oracle to perform testing.See also: action, action machine, trace, transition system.
test run bounds
Bounds on test runs during on-the-fly testing. Such bounds are controlled by switch clauses in the action machine definition or in a configuration on which the machine is based.See also: action machine, configuration, on-the-fly testing, switch.
test sequence
An ordered series of inputs to the system under test. Spec Explorer can generate a test sequence from a trace in a test oracle. A test case fails if the observed behavior of the system under test in response to a test sequence differs from the behavior in the associated trace.See also: action, test oracle, test sequence, trace.
test strategy
In Spec Explorer, the method used to construct from an input action machine a new action machine that is appropriate to use as a test oracle. Spec Explorer provides two test strategies: Short Tests and Long Tests.See also: action machine, construct behavior, test oracle.
test suite
A set of test cases. In Spec Explorer, a test suite is a set of test cases created to test the conformance of the system under test to the model and is the smallest unit of meaningful testing. Spec Explorer can generate a test suite from an action machine.See also: action machine, test case, test oracle.
test-enabled
Indicates that test code generation or dynamic traversal is available for an action machine. A machine is enabled for test code generation if its TestEnabled switch is set to true.trace
A valid sequence of steps in an action machine, as determined by the transition system generated by exploring the machine.See also: action machine, exploration, step, transition system.
transition
See definition for step.transition system
A collection of states and transitions between those states, called steps. In Spec Explorer, each step is labeled with an action invocation. Spec Explorer generates a transition system from an action machine through exploration.See also: action machine, exploration, state, step.
type binding
In Spec Explorer, a correlation between a model type and an implementation type. During test generation, model types are replaced with the correlated implementation type. The TypeBindingAttribute in a model program creates a type binding.See also: model program.
unexplored state
During exploration, any state that has been identified but for which outgoing steps have not been examined.See also: exploration, state, step.
universal behavior
One of the universal behavior operators, either the any action universal behavior or the any sequence universal behavior.See also: action, behavior.
update rule
See definition for rule.validation
A Spec Explorer feature that builds a solution containing a model and that looks for build errors and consistency issues. Distinct from model checking.