![]() |
![]() |
![]() |
![]() |
![]() |
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:
- Bit state exploration, an efficient algorithm for reasonably large SDL systems.
- Random walk, a simple algorithm that can be used for very large SDL systems.
- Exhaustive exploration, an algorithm suited only for small SDL systems.
The characteristics of these algorithms are further described in Configuring the SDL Explorer. They have the following in common:
- They start from the current system state, which means that you may have to navigate to a suitable start state before the exploration is started.
- They explore the state space down to a certain depth from the start state, to avoid exploring an infinite state space forever.
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:
- To start a bit state exploration, enter the command
Bit-State-Exploration, or click the Bit-State button.- To start a random walk, enter the command Random-Walk, or click the Random Walk button.
- To start an exhaustive exploration, enter the command
Exhaustive-Exploration (there is no button for this command).
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 : 100Hash table size : 1000000 bytes** Starting exhaustive exploration **Search depth : 100** Starting random walk **Depth : 100Repetitions : 100By 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.
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:
- No of reports: x
The number of error situations found. How to investigate the reports are described in Examining Reports.- Truncated paths: x
The number of times the exploration reached the maximum search depth. The execution path is at that stage truncated and the exploration continues in another state. If this value is greater than 0, parts of the state space have not been explored. However, this is a normal situation for SDL systems with infinite state spaces.- Collision risk: x
For bit state explorations, the risk (in percent) for collisions in a hash table used to represent the generated system states (see Bit State Exploration Options). This value should be very small, 0-1%; otherwise, the size of the hash table may have to be increased. If collisions occur, some execution paths may be truncated by mistake.- Current depth: x
The search depth reached at the moment the exploration was finished or stopped. If this value is -1, the exploration finished by itself. If the depth is greater than 0, the exploration was stopped. In this case, it may be continued from this depth, as described in Executing an Exploration.- Symbol coverage: x
The percentage of the SDL symbols in the system that have been reached during the exploration. If this value is less than 100, parts of the system have not been explored.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.
The nodes in the Report Viewer are structured in three levels and show, from top to bottom:
- The total number of generated reports
- The different types of reports (errors) and the number of reports of that type
- The actual reports with error message and trace information, and the exploration depth where the error was generated (this level of the tree is by default collapsed).
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:
- Expand the report structure to show the desired report node.
- 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:
- List the reports by entering the command List-Reports, and note the number of the desired report.
- 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 |
![]() |
![]() |
![]() |
![]() |