IBM
Contents Index Previous Next



Underlying Principles and Terms


The SDL Explorer is based on a technique called state space exploration, which is a well-known technique for automatic analysis of distributed systems. All state space exploration tools for SDL are based on the idea of an automatic generation of the reachable state space for the SDL systems.

For readers interested in a more detailed description of the possibilities given by state space exploration for validation of distributed systems (focused on protocols), an excellent description is given in [17], see References.

Behavior Trees

The SDL Explorer operates on structures known as behavior trees or reachability graphs. A behavior tree is a tree structure that represents the behavior of an SDL system.

The nodes of the tree represent SDL system states. A system state is defined by:

The edges between the nodes in the tree represent atomic SDL events that transfers the SDL system from one system state to another. Therefore, the edges are also called behavior tree transitions. They can be individual SDL statements like tasks, inputs, outputs, etc. but also complete SDL transitions, depending on how the Explorer is configured.

The size and structure of the behavior tree can thus vary and is determined by a number of Explorer options. These options affect the number of system states generated for an SDL transition, and the number of possible behavior tree transitions from a state in the tree.

State Space Explorations

The set of all system states represented by the behavior tree is called the state space of the system. By moving around in the behavior tree, the behavior of the SDL system can be explored and the system states reached can be examined. This is known as state space exploration, and it can be performed both manually and automatically.

Note:

The "children" of a node in the behavior tree are not generated until a state space exploration actually reaches that node, i.e., the tree is not a static structure generated when a explorer is started.

For each system state reached during state space exploration, a number of rules are checked to detect errors or possible problems in the SDL system. If a rule is violated, a report is generated to the user. By investigating the report and the system state where it was generated, the cause of the error can be determined.

States and Paths

The original start state of the system is called the system start state. It is the system state where the static process instances have been created but their initial start transitions have not been executed.

The current state is the system state that currently is under investigation. It is changed when manually navigating in the behavior tree, or when going to the system state where a report has been generated. Initially, it is set to the system start state.

The current root of the behavior tree can be any system state. A number of Explorer commands and features use it as a starting point of operation. Initially, it is set up to the system start state, also known as the original root of the behavior tree. If it is redefined, it is not possible to reach a state above the current root in the behavior tree without resetting it back to the original root.

A path between two states in the behavior tree can be denoted by a sequence of integers, each one indicating which transition was used to get between two states in the path. The current path is a path that is set up when manually navigating in the behavior tree, or when going to the system state where a report has been generated. When set up, it is the path between the current root and the current state. The current path is changed when the Explorer moves to a state that is not part of the current path, e.g. when manually navigating to a system state outside of the current path. However, moving up and down along the current path does not change it.


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