IBM
Contents Index Previous Next



Defining Signals from the Environment


A problem common to all state space exploration techniques is related to the treatment of the environment of the SDL system under analysis. As an example, consider the situation during state space exploration where a signal with an integer parameter can be received from the environment. Since there is an infinite number of integer values, there will be an infinite number of successors of the current system state: one where the parameter value is 0, one where the parameter value is 1, etc.

This is obviously a situation that is not acceptable when performing state space exploration. The SDL Explorer allows three different strategies to avoid situations like this:

  1. Create a closed system by specifying the environment of the system using SDL. This will solve the problem but introduces a new one; it is necessary to create an SDL model of the environment.
  2. Specify the signals that can be sent from the environment to the system. This is a simple way to avoid the problem. By enumerating the signals with their parameters that the environment can send, a finite branching is guaranteed at each system state in the state space.
  3. Use an MSC to guide the state space exploration. Since the MSC defines what signals the environment can send and their ordering, a limited part of the state space can be explored.

The second strategy is the most common and the test value feature of the Explorer is designed to make it easy to define the signals from the environment.

Test Values

When the Explorer is started a list of signals is automatically computed that will be used as the possible signals from the environment during state space exploration. The signal list is generated based on the concept of test values. Test values can be defined for data types and for signal parameters. When generating the signal list the Explorer checks for each signal that can come from the environment which test values are defined for its parameters (or for the parameter data types). It then generates one signal instance for each combination of test values for the parameters.

Each time the Explorer is in a state where input from the environment is possible during state space exploration, the list of signals defined by the test values is consulted.

The default test values for the simple data types are:

Data Type Default Test Values
Integer

-55, 0, 55

Boolean

true, false

Real

-55, 0, 55

Natural

0, 55

Character

`a'

Charstring

"test"

Duration

0

Time

0

PId

Environment PId

Bit

0, 1

Octet

00, FF

Bit_string

'01'B

Octet_string

'00FF'H

For other data types, test values are determined according to the following:

Test Values Restrictions and Options

Two restrictions are posed on the computed test values:

Two commands exist for setting options related to the above restrictions:

Note:

These options affect the state space; see Affecting the State Space.

Defining and Listing Test Values

The default test values are defined to be useful for a large number of applications, but they sometimes need to be modified. In some cases there are unnecessarily many test values and to enhance the performance of the state space exploration some test values can be cleared. In other cases the automatic test value generation cannot handle some of the data types used, so the test values must be manually defined.

Changing the test values are therefore only needed if you would like to fine-tune the behavior of the Explorer, or if the signals from the environment have parameters that are of a user-defined or unusual data type.

Note:

Changing test values affects the state space; see Affecting the State Space.

Test values can be defined and cleared on three "levels": on data types, on individual signal parameters, and on signal instances. When test values are defined or cleared, the list of signals from the environment is regenerated. You are recommended to define test values either on data types and individual signal parameters, or on signal instances; do not combine both these methods.

The monitor commands concerning test values are available in the Test Values module in the Explorer UI.

Test Values for Data Types

The following commands operate on the test values for a data type (sort).

Test Values for Signal Parameters

The following commands operate on the test values for individual parameters to a signal.

Test Values for Signal Instances

The following commands operate on the test values for a specific signal instance.

Note:

The signals defined using this command are cleared when the signal list is regenerated, e.g. if a test value is defined for a sort or a signal parameter.

Saving Test Values

The current set of test values can be saved on file and later be recreated by reading in the file again. The file will contain monitor commands that recreates the saved set of test values and discards any other test values.

To save the test values, enter the command Save-Test-Values, followed by a file name. To read in the saved test values again, enter the command Include-File, followed by the file name.


http://www.ibm.com/rational
Contents Index Previous Next