![]() |
![]() |
![]() |
![]() |
![]() |
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:
- 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.
- 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.
- 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:
Integer Boolean Real Natural Character Charstring Duration Time PId Bit Octet Bit_string Octet_stringFor other data types, test values are determined according to the following:
- Enumerated types: All values in the type
- Subranges of the predefined data types: All values in the range
- Structures: All combinations of the test values of the individual fields
- Arrays: All combinations of the test values of the component type.
- Ref types: NULL + pointers to the test values for whatever the Ref points to.
- Own types: NULL
- ORef types: NULL
Test Values Restrictions and Options
Two restrictions are posed on the computed test values:
- If the number of test values for a data type or signal parameter exceeds a maximum number, randomly chosen test values will be generated.
- If the number of signal instances for a particular signal type exceeds a maximum number, randomly chosen signal instances will be generated for this signal type.
Two commands exist for setting options related to the above restrictions:
- To define the maximum number of test values for any data type or signal parameter, enter the command Define-Max-Test-Values, followed by the number of test values. The default is 10.
- To define the maximum number of signal instances for any signal type, enter the command Define-Max-Signal-Definitions, followed by the number of signal instances. The default is 10.
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.
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).
- To define a new test value for a sort, enter the command
, or click the Def Value button. The parameters are the sort and the value. Example:integer 20- To list the new test values defined for all sorts, enter the command List-Test-Values, or click the List Value button.
- To clear all test values for a sort, enter the command
Clear-Test-Values, or click the Clear Value button. As parameter, you either specify the sort, or `-' which means all sorts.Test Values for Signal Parameters
The following commands operate on the test values for individual parameters to a signal.
- To define a new test value for a signal parameter, enter the command Define-Parameter-Test-Value, or click the Def Par button. The parameters are the signal, the ordinal number of the signal parameter, and the value. Example:
Define-Parameter-Test-Value Score 1 -5- To list the new test values defined for all signal parameters, enter the command List-Parameter-Test-Values, or click the List Par button.
- To clear all test values for a signal parameter, enter the command
Clear-Parameter-Test-Values, or click the Clear Par button. As parameter, you specify the signal and the ordinal number of the signal parameter. You may use `-' for the parameter number, which means all signal parameters, or just `-' for the signal, which means all signal parameters for all signals.Test Values for Signal Instances
The following commands operate on the test values for a specific signal instance.
- To define a new set of test values for a signal instance, enter the command Define-Signal, or click the Def Signal button. The parameters are the signal and an optional set of values for the parameters. Multiple Define-Signal commands may be used to define several signal instances of the same signal type, but with different values. Example:
Define-Signal Test 10 'hello' trueDefine-Signal Test -5 'bye'
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.
- The command Extract-Signal-Definitions-From-MSC analyzes basic MSCs in textual form (with suffix .mpr) and extracts all signals sent from the environment axes to the system axis. If a signal definition is found which does not already exist, it is added automatically by calling Define-Signal.
- To list all currently defined signal instances, enter the command List-Signal-Definitions, or click the List Signal button.
- To clear all test values for a signal type, enter the command
Clear-Signal-Definitions, or click the Clear Signal button. As parameter, you specify the signal, or `-' which means all signals.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 |
![]() |
![]() |
![]() |
![]() |