IBM
Contents Index Previous Next



Performing Automatic State Space Explorations


This section describes how to perform an automatic state space exploration and how to examine the results. The application areas in which automatic state space exploration are used are further described in Validating an SDL System, Verifying an MSC, Using Observer Processes and Using Autolink.

In the Explorer, three types of automatic state space explorations can be used, implemented as different algorithms:

The characteristics of these algorithms are further described in Configuring the SDL Explorer. They have the following in common:

The performance and results of a state space exploration are also highly dependent on how the state space is configured. This is discussed in State Space Options.

The most important monitor commands concerning state space explorations are available in the Explore module in the Explorer UI.

Executing an Exploration

The different types of explorations are started in the following way:

Note:

The button Verify MSC starts a bit state exploration, configured to suit MSC verification. This is further described in Verifying an MSC.

When the exploration is started, a message is printed stating the options used for this exploration type (see Configuring the SDL Explorer):

** Starting bit state exploration **
Search depth    : 100
Hash table size : 1000000 bytes


** Starting exhaustive exploration **
Search depth : 100


** Starting random walk **
Depth       : 100
Repetitions : 100

By default, the exploration continues until it is finished, i.e., until the state space has been fully explored according to the exploration options. During the exploration, a status message is repeatedly printed after a certain number of transitions or states have been generated.

Note:

Depending on how an exploration is configured, it may take a considerable amount of time to finish!

To stop an exploration manually, click the Break button in the Explorer UI, or hit <Return> in stand-alone mode. A stopped exploration may be continued by issuing the same exploration command again. You are then asked whether to continue the exploration from the state where it was stopped, or restart the exploration from the same start state as before.

When the exploration is finished or stopped, some exploration statistics are printed (see Interpreting Exploration Statistics). By default, a tool called the Report Viewer is also opened (see Examining Reports).

The Explorer always returns to the start state of the exploration when it is finished or stopped.

Rules Checked During Exploration

During state space exploration, a number of rules are checked to detect errors or possible problems in the SDL system. If a rule is satisfied, a report is generated to the user.

The rules are used to find design errors, typically caused by unexpected behaviors of the SDL system. Often the errors are caused by events happening at the same time in different parts of the system, for example when a signal is received from the environment of the system at the same time as a timer expires. So-called signal races are often part of the error situations that are found.

Apart from the predefined rules, an additional rule can be defined by the user to check for other properties of the system. See Using User-Defined Rules for more information.

Interpreting Exploration Statistics

The different exploration algorithms print somewhat different statistics. The important statistics to note are the following:

What actions to take depending on the printed statistics is discussed in Validating an SDL System.

Examining Reports

When an exploration has been performed, the reported error situations should be examined. A dedicated graphical tool, the Report Viewer, is available in the Explorer to facilitate the report examination. However, it is possible to examine the reports without using the Report Viewer.

The Report Viewer is by default automatically opened when an exploration has been performed. To open the Report Viewer manually, either select Show Report Viewer from the Commands menu, or enter the command Show-Report-Viewer.

Figure 488 : The Report Viewer

The nodes in the Report Viewer are structured in three levels and show, from top to bottom:

To close the Report Viewer, click the Close quick button in the tool bar.

To list the reports when the Report Viewer is not opened, enter the command List-Reports, which prints a numbered list of all reports.

Changing the Displayed Structure

Generally, to expand or collapse a node in the Report Viewer, double-click the node or select Expand or Collapse from the popup menu available on the nodes. This works for the top node and the report type nodes; for report nodes, see Going to a Report (below).

To show the whole report structure, select Expand Substructure from the popup menu available on the top node. To collapse the whole structure, select Collapse from the same pop-up menu, or double-click the expanded top node.

To switch between a tree structure and a list structure, click on the Structure quick button. The list structure makes it possible to easier see the different reports and report types when a large number of reports have been found.

Going to a Report

When "going to a report," the Explorer goes to the system state where the report was generated. You can then examine the reported situation further.

To go to a report using the Report Viewer:

  1. Expand the report structure to show the desired report node.
  2. Double-click the report node, or select Goto from the pop-up menu available on the report node.

To go to a report using monitor commands:

  1. List the reports by entering the command List-Reports, and note the number of the desired report.
  2. Enter the command Goto-Report, followed by the report number.

After going to a report, the Navigator tool is updated and the current path is set up. You can walk along the path to the error by using the Navigator; see Moving Along the Current Path.

By default, an MSC Editor is also opened, showing the MSC trace from the current root to the state where the report was generated.


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