![]() |
![]() |
![]() |
![]() |
![]() |
Validating Large Systems
This section discusses various techniques that are useful when designing and validating large SDL systems. A large system is, in this context, a system that has a state space that is too large to be completely explored using one automatic state space exploration. The techniques are pragmatic and intended to give a reasonable chance of finding any errors even though the complete state space is not searched.
The following techniques are discussed:
- Decomposed Exploration
- Using MSCs to Limit the Search
- More Efficient Bit-State Exploration
- Reducing the State Space Size
- Using Random Walk Exploration
- Incremental Validation.
Decomposed Exploration
The idea when using decomposed explorations is to use a number of reasonably small explorations instead of one big exploration. Quite often the behavior of an SDL system can be divided into a number of "phases" or "features." The idea is to explore each of these phases or features separately. The benefit with this approach is that it is a lot easier to explore the different phases separately than trying to explore the combination of all phases. The drawback is that errors that are caused by an interaction between different phases or features are not found. However, for large SDL systems it is sometimes the only possible method that at least can give a complete symbol coverage.
The process of finding which and how many partial explorations that are necessary is a combination of an iterative process and a planning issue where the possible features and phases that can be subject to a partial exploration are identified. If an incremental design process is used it is often possible to use the different iterations to guide the choice of partial explorations; compare with Incremental Validation.
A common strategy used to find the needed partial explorations is essentially the following:
- Start an exploration from the system start state.
- Check all reports and correct the errors in the system. Generate a new explorer and make another exploration.
- When all found reports have been fixed, check the symbol coverage. If the coverage is 100%, the validation is finished; otherwise, continue with the next step.
- Use the Coverage Viewer to check which parts of the SDL system that need more testing.
- Go to a suitable system state and start a new exploration from there.
- Repeat the process until the symbol coverage is 100%.
There are two issues of this strategy:
Where to Start a Partial Exploration
The problem of identifying where to start a new exploration is of course system dependent and requires knowledge of the SDL system. The tool to use in this case is the Coverage Viewer, which shows exactly what parts of the SDL system that have been executed during the exploration and what parts have not been executed. Once a system state has been chosen the next issue is how to get there in the Explorer. There are number of possible ways to do this; see Going to a System State.
How to Limit a Partial Exploration
The next problem is to limit each partial exploration to the intended part of the state space. There exists a number of factors which can be used to influence the extent of an exploration:
The search depth is the simplest limiting factor to use. By reducing the search depth, e.g. to 10 or 20, the size of the exploration will of course be considerably reduced compared to the default depth of 100.
By changing the list of signals that can be sent from the environment it is possible to control which parts of the system that will be exercised by an exploration. For example, if we are interested in testing the data transfer phase of a connection-oriented protocol specification, a good strategy would be the following:
- Go to a system state where the connection is established.
- Define the signals from environment to be only the signals relevant for the data transfer, and start the exploration. For a description of how to define and remove signals from the list of signals that can be sent from the environment, see Defining Signals from the Environment.
User-defined rules also give a possibility to limit the extent of an exploration. Define a rule that matches the system states where the exploration should be pruned and check that the report action for user-defined rules is to prune the search. For example, the rule
state(initiator:1)=idle would prune the exploration whenever the initiator process entered the state Idle. User-defined rules are described in Using User-Defined Rules.Using MSCs to Limit the Search
Another possibility that sometimes is useful to control the exploration of the state space is to use MSCs to guide the exploration. This is particularly useful for SDL systems with a design that uses restrictions on the possible behavior of the environment of the system. It might, for example, be known that the signals A, B and C always will come in this order from the environment of the system. In this case it is not interesting to analyze what will happen if the signals will come in a different order.
An MSC can be loaded to guide the search by using the command Load-MSC. Once an MSC is loaded, both interactive navigation in the state space, e.g. by using the Navigator, and automatic exploration will only search the parts of the state space that correspond to the loaded MSC.
This means that if you want to go back to normal exploration, you have to clear the loaded MSC by using the commands Clear-MSC or Reset.
Note how the test values are used when an MSC is loaded. It is allowed to leave out parameters to messages in the MSC. If a parameter is left out on a signal from the environment, the test values are used to determine the parameter values that are actually sent to the system. This is a useful feature when using MSCs to limit the search. See section Verifying an MSC for more details.
Another useful hint when using MSCs is to always use system level MSCs to guide the state space exploration. A system level MSC will allow a larger part of the state space to be explored than a block or process level MSC.
An MSC loaded into the Explorer must comply with some requirements; see Requirements for MSC Verification.
More Efficient Bit-State Exploration
The bit-state search uses a hash value based algorithm to store the state space that is traversed. Unfortunately the computation of hash values from a system state is an expensive operation and most of the execution time in a bit-state search is spent calculating hash values. The execution time for the hash algorithm is in most situations proportional to the size of each system state. The max and min system state size used by the hash algorithm is included in the statistics printed after each bit state search and should be checked if the search is slow. (See Bit-State-Exploration).
If the size of a system state is big (> 10,000 bytes) the bit state execution of the explorer will be fairly slow. In these cases it might be worthwhile to try to optimize the performance by reducing the state size that the explorer uses when computing hash values. This can be done by informing the explorer to skip a number of variables when computing hash values. The explorer includes a command Define-Variable-Mode that is intended for this purpose. (See Define-Variable-Mode.) For example the command:
define-variable-mode monitor subscrTab skipwill make the explorer skip all subscrTab variables in monitor processes.
A typical example of where this feature is useful is if the system includes a big array (or other big data structure) that is initialized at the start up of the system and that after the initialization is known to be constant in the part of the state space that is explored. The correct way to take advantage of this in the explorer is to:
- Go to a system state where the array is initialized. (See Going to a System State for more info about how to navigate in the state space.)
- Redefine the root to the current state. (See Define-Root.)
- Change the mode of the table variable to "Skip".
- Start the bit-state exploration.
Using this strategy it is possible to considerably increase the performance of the explorer.
Another situation where the variable mode can be changed to "Skip" is when there are variables in the system that is known not to have any influence on the dynamic behavior of the system. See Variables Not Influencing the Dynamic Behavior.
Reducing the State Space Size
There is a number of ways to reduce the state space that is necessary to explore by using knowledge and assumptions about the SDL system. Usually this is based on the fact that the state space of an SDL system contains various "sub state spaces" that are equivalent except for some detail, which is not very interesting for the purpose of the validation. Some examples of such details are:
- The value of local variables
- The number of instances of process types
- The size of large data structures.
- Variables that do not influence the dynamic behavior.
Local Variable Values
An example of the way local variable values influence the size of the state space is the following: Consider a situation where a process contains an integer variable that counts the number of times a particular signal comes from the environment, and then replies with this number when requested to do so from the environment. It is obviously not especially interesting to try to investigate the behavior of the SDL system for all possible values of this local variable. Instead a reasonable set of values should be selected and the state space exploration guided by this selection.
A user-defined rule (see Using User-Defined Rules) provides an efficient means to reduce the size of the state space by putting restrictions on variable values. In the example above a reasonable restriction might be that we only would like check what happens the first three times the variable is increased. A rule that expresses this is:
proc:1->var < 4;Once this rule is defined and the report action for user-defined rule violation is set to Prune (which is the default), only the interesting parts of the state space are explored.
Number of Process Instances
Another issue is the number of process instances that are used for each process type. If the number is large and all of them do the same thing, for example by modeling different connections in a connection oriented protocol, it is probably not very useful to try to explore the combination of all instances. Instead, it is better to restrict the number of instances allowed in the exploration. This can be achieved with the command Define-Max-Instance (see Maximum Number of Instances). If preferred, it is also possible to use a user-defined rule or an observer process to achieve the same result.
Size of Large Data Structures
A third area where the explorer performance is reduced is when large data structures, e.g. arrays, are used in the SDL system. A large data structure has two unfavorable effects on a state space exploration:
- The size of the reachable state space increases extremely rapidly as the size of the data structure increases.
- The efficiency of the bit state algorithm is decreased as the size of system states increase. Essentially the time to compute a new system state is linear to the size of the system states.
A good idea in this context is to, whenever possible, try to reduce the size of any large data structures in the SDL system before performing validation. Another possibility is to skip the variable when computing hash values as described in More Efficient Bit-State Exploration.
Variables Not Influencing the Dynamic Behavior
In many situations an SDL system contains a number of variables that does not have any impact on the dynamic behavior of the system. Essentially all variables that does not (directly or indirectly) have any influence on the path taken through a decision or the expression used when computing the receiver of a signal in output/RPC call will not influence the dynamic behavior of the system.
These variables can safely be ignored when performing a state space search. This can be accomplished by instructing the explorer to skip these variables using the Define-Variable-Mode command. (See Define-Variable-Mode.) This will in many cases drastically reduce the size of the state space that the explorer needs to search and is an efficient way to improve the performance of the explorer.
Note that implicit variables like Sender/Parent/Offspring are also considered as variables in this respect. In particular Sender can be of interest to skip if it is not used, since it may change value every time a signal is received.
As an example, if Sender is not used in a process `p' the following command will make the explorer ignore the Sender implicit variable when comparing two system states:
define-variable-mode p Sender skipUsing Random Walk Exploration
In some situations it is not possible to use the more elaborated techniques described in this section to cope with the problem of validating large SDL systems. The time and resources available for the validation may simply be too limited. A possible strategy to use when validating very large SDL systems is to use the random walk exploration strategy instead of the bit state algorithm.
The reason is that the random walk algorithm gives a possibility to get a partial exploration of the state space that is randomly chosen. Furthermore, the symbol coverage of the exploration is determined only by how long the exploration is allowed to run. The drawback with the algorithm is that if it is allowed to run for a long time, so that significant parts of the state space already have been covered, there is no mechanism to avoid that already explored paths are explored once more.
How to start a random walk exploration is described in Executing an Exploration. The random walk exploration algorithm is further described in Random Walk Options.
The best way to get an idea of what has been tested when using random walk is to use the Coverage Viewer to check the symbol coverage. Even if this is not the same as the coverage of the system state space, it will show if there are large portions of the system that have not been reached by the exploration.
Incremental Validation
A common way to develop large SDL specifications and designs in practice is to use an incremental development strategy. First a base functionality is implemented and then various features are added in an incremental fashion. When this type of development process is used, a good way to plan the validation of the system is to let the different increments define the state space explorations that should be performed.
First a number of state space explorations are executed with different start states, and perhaps different test values. Together these explorations should give a good process graph coverage of the SDL system representing the base functionality.
For each increment that is added, a number of additional explorations is performed that will cover the new features in the SDL system.
It is also probably worthwhile to define command scripts that automatically can execute the various explorations that should be run to achieve a good process graph coverage. This makes it possible to run all of the various explorations in an straight-forward way for each new increment that is added to the system.
http://www.ibm.com/rational |
![]() |
![]() |
![]() |
![]() |