IBM
Contents Index Previous Next



Configuring the SDL Explorer


This section describe the various possibilities available to control the behavior of the Explorer using the options that can be defined for different features. The available options are grouped into a number of categories; each category and option will be described later in this section.

Managing Options

Each option can be set using a monitor command, usually named something similar to "Define-<option>". Most options can also be set from the menus Options1 and Options2 in the Explorer UI. The monitor command and menu choice associated with an option is listed together with the description of the option.

If the options are changed during a session with the Explorer, you will be asked whether to save the options when you exit or restart the currently executing explorer. If you save the options, the new values will be stored in a file named .valinit (on UNIX), or valinit.com (in Windows), in the directory from where the SDL Suite was started. This file will automatically be loaded the next time the Explorer is started from the same directory, thus restoring the previous options.

Some monitor commands operate on all the options:

Note:

This command also resets the explorer completely and is equivalent to restarting the explorer from scratch. To just set the options to their initial values without resetting the explorer:

  1. Set the options to their default values. See above.
  2. Read in the file .valinit (on UNIX), or valinit.com (in Windows); see above. Select Include Command Script from the Commands menu, or enter the command Include-File.

Affecting the State Space

Some of the options affect, directly or indirectly, the size of the state space and the structure of the behavior tree. This can only be done while being in the current root of the behavior tree, since the whole structure of the tree may be affected. If such an option is changed when the explorer is not in the current root of the behavior tree, you have two choices: either to change the current system state back to the current root, or to redefine the current root to the current system state.

In this case, the following dialog is opened:

Figure 491 : Changing the current root

To change the root to the current system state, select yes and click OK. (In stand-alone mode, enter yes)

To keep the current root and move back to it, select no and click OK. (In stand-alone mode, enter no)

Note:

It is not possible to cancel this operation, i.e. you have to either change the current root or the current system state.

Bit State Exploration Options

Bit state exploration is an efficient automatic state space exploration algorithm for reasonably large SDL systems (for a reference, see [17]). It performs a depth-first search through the state space and uses a bit array to store the states that has been traversed during the search.

Every time a new system state is generated during the search, two hash values are computed from the system state. The bit array is checked:

Search Depth

The search depth is the maximum depth the Explorer will explore a particular execution path in the state space. When this depth is reached, the search is truncated and the search backs up to a previous system state.

Hash Table Size

The size of the bit array used as hash table is an important factor defining the behavior of the bit state exploration. The reason is that each time a new state is checked by comparing its hash values with previous hash values there is a risk for collision. The bigger the hash table is, the smaller the collision risk is.

Random Walk Options

Random walk is an automatic state space exploration algorithm that can be useful for very large SDL systems. It performs a depth-first search through the state space by selecting transitions to execute at random.

When the maximum search depth is reached during such a "random walk," the search is restarted from the original state again and a new random walk is performed. However, there is no mechanism to avoid that already explored paths are explored once more, i.e. a system state may be visited a large number of times.

Search Depth

The search depth determines how many transitions will be executed before the search is pruned and restarted from the beginning again.

Repetitions

The number of times the random walk search will be repeated from the start state before the exploration is finished.

Exhaustive Exploration Options

Exhaustive exploration is an automatic state space exploration algorithm intended for small SDL systems where the requirements on correctness are very high.

The algorithm is a depth-first search through the state space similar to the bit state search, but there is no collision risk involved. The reason is that all traversed system states are stored in primary memory, so it is always possible to determine whether a newly generated system state has already been visited during the search.

The drawback with the algorithm is that very much primary memory is needed to be able to store all traversed states. This limits the complexity of the SDL systems the algorithm is applicable to.

Search Depth

The search depth is the maximum depth the Explorer will explore a particular execution path in the state space. When this depth is reached, the search is truncated and the search backs up to a previous system state.

MSC Verification Options

The MSC verification algorithm is a bit state exploration that is adapted to suit the needs of MSC verification:

Search Depth

The maximum depth searched by the algorithm. The intention is that this depth always should be enough. If the MSC verification fails and the number of truncations is more than 0, this depth should be increased.

Timer Check Level

When verifying an MSC where there are timers in the MSC and/or in the SDL system, there is a choice of how to perform the matching between the timer events in the MSC and in the SDL system. The timer check level determines how this matching should be done:

The choice must be determined by the style of MSC that is used.

This option affects the state space; see Affecting the State Space.

Report Options

For each report type, you can define the action performed when the report is found and whether it should be reported to the user.

Report Action

The report action determines what action should be performed when a report situation is encountered while performing state space exploration. There are three possibilities:

Note that for some report types, like Deadlock, the continue choice is impossible.

This option affects the state space; see Affecting the State Space.

Report Log

The report log setting defines whether the report should be recorded in the list of generated reports. If the report log is set to Off for a particular report type, these reports will never show up in the report list. Note however that the report action still is performed, even though the report is not logged.

This option affects the state space; see Affecting the State Space.

Report Viewer Autopopup

When an automatic state space exploration is finished, the Report Viewer is normally started automatically to present the found reports. In some cases this may be inconvenient, so there is a possibility to turn this feature off.

MSC Trace Options

When the Explorer performs an MSC trace, you can define what types of events that are traced.

Action Trace

By default, actions like tasks, decisions, etc. are not shown in the MSC trace. You may change this by setting action trace to On.

State Trace

By default, changes in process states are shown in the MSC trace by adding a condition symbol. You may change this by setting state trace to Off.

MSC Trace Autopopup

When you go to a report, an MSC Editor is normally started automatically to present the trace from the current root to the state where the report was generated. In some cases this may be inconvenient, so there is a possibility to turn this feature off.

State Space Options

The structure and size of the state space that can be generated for any given SDL system can be modified in a number of ways using the state space options. The default values are defined to make the state space as small as possible to make the Explorer immediately useful for as many applications as possible. This, however, also means that the search performed by the Explorer is fairly scarce compared to what is possible. Some error situations may thus be overlooked during the search if they only occur in a part of the state space that never is reached.

Since these options affect the state space, note the information in Affecting the State Space.

Transition Type

There are two alternatives possible for the type of a behavior tree transition during state space exploration:

If it is equal to an SDL process graph transition, whenever such a transition is started, it is completed before anything else is allowed to happen. This implies that all process instances in all system states in the behavior tree will always be in an SDL process graph state.

If it is only a part of an SDL process graph transition, a transition in the behavior tree is considered to be a sequence of events that are local to the process instance, followed by a non-local event. Examples of local events are tasks and decisions; examples of non-local events are creates and inputs/outputs of signals from/to other process instances. The idea of this alternative is to model the ITU semantics for SDL as closely as possible while still allowing optimized performance during state space exploration.

Scheduling Algorithm

The scheduling algorithm defines which of the process instances in a system state will be allowed to execute. There are two possible alternatives:

The ready queue is a queue containing all process instances that have received a signal that can cause an immediate transition, but that have not yet had the opportunity to execute this transition to its end.

If all process instances are allowed to execute, the semantics of ITU recommendation Z.100 are modeled. There will be one child node to the current node in the behavior tree for each process instance in the ready queue.

If only the first process instance is allowed to execute, the semantics of an application that has been generated by the SDL to C Compiler are modeled. There will only be one child node to the current node in the behavior tree, the first process instance in the ready queue.

Event Priorities

The events that are represented in a behavior tree can be divided into five classes:

To each of these event classes a priority of 1, 2, 3, 4 or 5 is assigned. These priorities are used during state space exploration to determine which transitions should be generated from each system state. The events with priority 1 are first considered. Only if no events with priority 1 are possible in the current state, the events with priority 2 are considered. Only if no events with priority 1 or 2 are possible in the current state are events with priority 3 considered, etc.

Note that also the setting of the symbol time option will have an impact on the events that will can be executed in each system state; see section Transition Time.

The two most common ways of assigning priorities to event classes are:

The first alternative represents the situation where no assumptions can be made about the time scale for the different types of events. The second alternative represents a situation where the internal delays are very short compared to the timeout durations and execution speed of the environment.

Transition Time

A common simplification made in the analysis of SDL systems is to consider the time it takes for a process to execute a symbol, e.g. an action or output, to be zero. This time is of course never zero in a real system, but in many cases the time is very small compared to the timer durations in the system, and can be neglected when analyzing the system.

Consider for example a situation where a process sets a timer with a duration 5 and then executes something that may take a long time, e.g. a long loop, and then sets a timer with duration 1. If symbol time is assumed to be zero, the second timer will always expire first. If considered to be non-zero, any one of the timers can potentially expire first.

The explorer allows the user to choose whether to assume that the execution time for SDL symbols is zero or undefined using the Define-Symbol-Time command.

Channel Queues

The Explorer allows queues to be attached to and removed from all channels in the SDL system. If a queue is added for a channel, it implies that when a signal is sent transported on this channel it will be put into the queue associated with the channel. Then there will be a separate transition in the state space that represents the forwarding of the signal to the receiver (or the next channel queue).

Maximum Input Port Length

The length of the input port queues is not infinite in the Explorer, since in practice it is likely to be a design error if the queues grow forever. If the length of a queue exceeds the defined max length during state space exploration, a "MaxQueuelength" report is generated.

Maximum Transition Length

To make it possible to detect infinite loops within a transition in the state space, the maximum number of SDL symbols allowed to be executed in one transition is defined. If this number is exceeded during state space exploration, a "MaxTransLen" report is generated.

Maximum Number of Instances

To avoid infinite chains of create actions in the state space, the Explorer uses a max number of allowed process instances for any type. If this number is exceeded during state space exploration, a "Create" report is generated.

Maximum State Size

When the Explorer is exploring the state space, an internal buffer is used to store the system states. The size of this buffer defines the maximum size of the system states that the Explorer can handle.

Timer Progress

One test that can be made with the Explorer is to look for non-progress loops, i.e. loops in the state space without any progress being made. The intention with this test is to look for situations where the SDL system is busy doing internal communication but to an outside observer looks dead.

This option defines if the expiration of a timer is considered as progress when performing non-progress loop checking. See also Non Progress Loop Error.

Spontaneous Transition Progress

One test that can be made with the Explorer is to look for non-progress loops, i.e. loops in the state space without any progress being made. The intention with this test is to look for situations where the SDL system is busy doing internal communication but to an outside observer looks dead.

This option defines if a spontaneous transition is considered as progress when performing non-progress loop checking. See also Non Progress Loop Error.

Autolink Options

See section Computing Test Cases for a discussion of the Autolink options.

Setting Advanced Options

Advanced options can be set for state space explorations to achieve a much larger state space than the default, thus allowing for special kind of errors to be detected. See Using Advanced Validation for more information.

To set advanced options, click the Advanced button in the Explore module. This executes the following set of commands:

Define-Scheduling All
Define-Priorities 1 1 1 1 1
Define-Max-Input-Port-Length 2
Define-Report-Log MaxQueuelength Off

The reasoning behind these settings are:


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