IBM
Contents Index Previous Next



Validating an SDL System


This section describes how to use the automatic state space exploration facilities in the Explorer to look for inconsistencies and design errors in an SDL system. The idea is essentially to test the robustness of the application, the responses to unexpected situations. Essentially the validation is an attempt to answer questions like:

...and all other questions the designer never ever would imagine.

It is assumed that the SDL system is of moderate size and complexity; techniques for validating large SDL systems are described in Validating Large Systems.

Using a Default Exploration

When you are to use the Explorer to try finding errors in a new SDL system for the first time, you are advised to start a bit state exploration using the default options.

To validate a system opened in the Explorer:

  1. If you already have executed commands for the opened explorer, you should reset the explorer. Enter the command Reset, or click the Reset button in the Explore module. This is especially important if you earlier have loaded an MSC into the Explorer.
  2. You should also make sure you use the default state space and exploration options. Enter the command Default-Options, or click the Default button in the Explore module.
  3. Start a bit state exploration (see Executing an Exploration). Let the exploration run for at least 10-20 minutes.
  4. If the exploration has not finished by itself, stop it manually (see Executing an Exploration). The Report Viewer is opened and the exploration statistics is printed. Note especially what the symbol coverage is.
  5. Use the Report Viewer to go to each of the reported situations (see Examining Reports). Navigate along the current path to the report and use the tracing and viewing facilities to examine the report.
  6. If you find errors in the system, you may decide to correct them immediately. In that case, generate a new explorer for the corrected system and rerun the validation, as described above. Otherwise, you should check if the validation is to be considered finished (see below).

Determining if the Validation is Finished

When all reports have been checked and the found errors possibly have been corrected, the next question arises: When are we finished validating the system? To answer this question, look at these aspects:

The following possibilities now exist:

  1. The symbol coverage is 100% and the exploration finished by itself.
    All symbols have been executed and furthermore most orderings of the possible actions have been tested. In this case it is probably not worthwhile continuing the validation; you may consider it finished.
    However, not all orderings of possible actions have been tested, since the search may have been truncated, collisions may have occurred in the hash table, and more orderings are possible by configuring the state space exploration differently. If you want, you can change the explorer options and start a new exploration (see Using Advanced Validation and Configuring the SDL Explorer).
  2. The symbol coverage is 100% but the exploration was manually stopped.
    In this case, it may still be worthwhile to continue the exploration until it finishes by itself. More reports may be generated, as there are still orderings of the possible actions that have not been executed.
  3. The symbol coverage was less than 100%.
    Parts of the system have never been reached during the exploration. In this case, the validation cannot be considered finished, even if the exploration finished by itself. The reasons and possible solutions for low symbol coverage are discussed next.

Handling Low Symbol Coverage

If the symbol coverage after an exploration is 100%, all parts of the system have been executed at least once. If the symbol coverage is less than 100%, the possible reasons why parts of the state space have not been reached are listed below.

To find out which parts of the system that have not been reached, a tool called the Coverage Viewer is used. To start the Coverage Viewer, select Show Coverage Viewer from the Commands menu, or enter the command Show-Coverage-Viewer. If the symbol coverage was less than 100%, the Coverage Viewer will display a tree structure representing the parts of the system that have not been executed.

Using Advanced Validation

The default options for the state space exploration, in particular the options that define the structure of the state space, are optimized to give good results for a first validation of a system. They are intended first of all to test for internal inconsistencies in the SDL system and to get a good process graph coverage. This assumes a reasonably "nice" environment, i.e., the environment only sends signals when nothing can happen internally in the system.

This has the benefit of reducing the size of the state space while still preserving a good process graph coverage. The drawback is that some error situations are never detected. One particular class of errors that never will be detected using the default options can be characterized as signal races caused by signals sent from the environment, or timer expirations that happen at the same time. An example is a situation where a communication protocol ends up in an inconsistent system state when two connect requests are sent to the different access points at the same time.

To detect these types of errors it is necessary to change the options and perform a second set of explorations for the SDL system. The suitable settings of the options are called advanced options. When using these values for the options, the state space will get very large for most SDL systems. It is thus usually not possible to get a complete coverage of the state space, even if some of the techniques described in Validating Large Systems have been used. To anyway be able to get good results, the best strategy is to use the random walk algorithm when exploring the state space. See Using Random Walk Exploration for more information.

To set advanced options, click the Advanced button in the Explore module. In stand-alone mode, you have to enter a number of commands to achieve the same result; see Setting Advanced Options for information on which commands to use.

For a more in-depth explanation of the state space options, see State Space Options.


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