Symbolic Exploration

This feature is experimental in the current release.

Symbolic values are names that represent values. They are introduced by parameters and scenario variables that are not fully expanded (that is, not given concrete values) at the time of model exploration. At test-run time, symbolic values are instantiated with concrete values that come from the system under test.

Spec Explorer automatically extracts restrictions on the allowable values for unexpanded data from the model in the form of state constraints, step constraints, and preconditions. State constraints are all conditions that must be true about symbolic values when the model is in that state. Preconditions are conditions that must be true for a step to be taken in a test. Step constraints are restrictions on symbolic values introduced by an exploration step.

State constraints are displayed in the State Browser when a state is clicked in the Exploration Graph Viewer. Preconditions and step constraints are displayed in the Step Browser when a step is clicked in the Exploration Graph Viewer.

Test cases generated by Spec Explorer automatically confirm that constraints are correctly honored and enforce preconditions. The actual values returned by the system under test must meet the expressed step constraints of one of the possible responses, or a conformance error results and the test case fails. Subsequent stimuli will be chosen from those whose preconditions are met by those values.

This release of symbolic exploration is an upgrade of prior symbolic functionality and is still an experimental feature. It provides an alternative to the previously recommended abstract identifier pattern where the adapter had the responsibility to dynamically bind values from the system under test.

See Also

Concepts

Exploration