Table of Contents

Previous Chapter

8 Validating a System

Introduction

Application Areas

• It provides an automated fault detection mechanism that finds inconsistencies and problems in an early stage of development. This is often referred to as validating an SDL system. See "Validating an SDL System" on page 401.
  
• When verifying the system against requirements, the Validator provides a possibility to perform automatic verification of the requirements expressed using the MSC (Message Sequence Chart) notation. See "Verifying an MSC" on page 411.
  
• When designing safety-critical or complex systems the Validator provides a possibility to test specific properties of the design. See "Using Observer Processes" on page 415.
  

Structure of a Validator

The same interactive monitor system as for a simulator is used, but the set of available commands differ. The graphical user interface to the validator monitor, the Validator UI, works in the same way as the Simulator UI, but the set of available command buttons differ. For a description of some other differences, see "The Validator User Interface" on page 384.

Underlying Principles and Terms

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 [1], see "References" on page 442.

Behavior Trees

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

• The process instances that are active
  
• The variable values of these processes
  
• The SDL control flow state of the process instances
  
• Any procedure calls (with local variables etc.)
  
• Signals (with parameters) that are present in the queues of the system
  
• Active timers
  
• Etc.
  

The size and structure of the behavior tree can thus vary and is determined by a number of Validator 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

------------------------------------------------------------------------
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 validator is started.             
------------------------------------------------------------------------

States and Paths

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 Validator 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 Validator 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.

Generating and Starting a Validator

• A quick way in one single step, adequate for most situations
  
• A more complex way in several steps, giving you complete control of the generation and start process.
  

Generating a Validator

To generate an executable validator:

1. Select Make from the Organizer's Generate menu. The Make dialog is opened.
   
2. Turn on the options Analyze & generate code and Compile & link.
   
3. From the Standard kernel option menu, select Validation.
   
4. If you need to check the Analyzer options, click the Analyze Options button. In the dialog, set the options and click the Set button. For more information about these options, see "Analyzing using Customized Options" on page 312.
   
5. Click the Make button.
   A validator for the system is now generated in the current directory with the name <system>_xxx.val (the _xxx suffix is platform specific). The Status Bar of the Organizer reports the progress of the generation; the last message should be "Compiler done."
   
6. Open the Organizer Log window from the Tools menu and check that no errors occurred and that a validator was generated.
   
   • If errors were found, correct them and repeat the generation process. See "Locating and Correcting Analysis Errors" on page 316.
     
   • If no validator was generated, repeat the generation process, but click the Full Make button in the Make dialog instead.
     

Starting a Validator

Graphical Mode

To start a validator in graphical mode:

1. Select Validator UI from the Organizer's Tools menu. The graphical user interface of the Validator is opened (see "The Graphical Interface" on page 385).
   
2. Select Open from the Validator UI's File menu. A Standard File Selection Dialog dialog is opened.
   
   • Alternatively, click the Open quick button in the tool bar.
     

3. In the dialog, locate and select an executable validator and click OK.
   A welcome message is printed in the text area of the Validator UI. The monitor system is now ready to accept commands.
   

Stand-alone Mode (Textual Mode)

To start a validator in stand-alone mode, the generated validator is executed directly from the OS prompt, e.g.

csh% ./system_vla.val

Welcome to SDT VALIDATOR
Command :

--------------------------------------------------------------------
Note:                                                                 
Before a validator can be run in stand-alone mode, you must execute   
a command file from the operating system prompt. The file is called   
telelogic.sou or telelogic.profile and is located in the              
SDT binary directory that is included in your $path variable.

        
For csh-compatible shells: source <bin dir>/telelogic.sou

      
For sh-compatible shells: . <bin dir>/telelogic.profile         
--------------------------------------------------------------------

Quick Start of a Validator

To quick start a validator, click the Validate quick button in the Organizer's tool bar. The following things happen:

• A validator is generated by using the validator kernel that is specified in the Make dialog. (If no validator kernel is specified, a default validator kernel is used.)
  
• The graphical Validator UI is started.
  
• The generated validator is started from the Validator UI.
  

Restarting a Validator

• In graphical mode, select Restart from the Validator UI's File menu. (This is the same as opening the same validator again.) A confirmation dialog is opened.
  
• In stand-alone mode, the validator has to be exited with the Exit command and then executed from the OS prompt again.
  

Actions on Validator Start-up

In some cases when the Validator is started, a message is printed that it is not possible to generate test values for all sorts and/or signal parameters. This has to do with the automatic test value generation mechanism that is used in the Validator. It happens if there are signals coming from the environment of the SDL system that have parameters of a sort that the test value generation cannot handle. To overcome this, define some test values for the sort that the Validator is complaining about. See "Defining Signals from the Environment" on page 421 for more information.

The Validator User Interface

The Validator UI can be customized in the same way as the Simulator UI. Please see "Customizing the Simulator UI" on page 337 for more information.

However, there are a few differences between the user interface of the Validator and the Simulator. These differences are described below.

Activating the Monitor

These conditions are listed in greater detail in "Activating the Monitor" on page 1888 in chapter 33, The Validator.

The Graphical Interface

Figure 180 : The Validator UI. 
-----
(fig)  
       
-----

The Command and Watch Windows

• In the Command window, the default commands that are executed are "List-Process -" and "Print-Trace 1".
  
• In the Watch window, a variable specification consists of the process instance name without parenthesis, followed by the variable name, e.g. game:1 count.
  

Navigating in the State Space

The Navigator is intended to be used in three different situations:

1. When learning how a state space exploration tool like the Validator works, the Navigator is a convenient tool for interactively investigating the behavior tree of an SDL system.
   
2. When using automatic state space exploration, there is sometimes a need to start the exploration from a different starting point than the system start state of the SDL system. In this case, the Navigator can be used to walk to a suitable system state, from which the automatic exploration can be started.
   
3. When investigating a report generated during automatic exploration, the Navigator can be used to check the alternative behaviors that are possible on the path to the reported situation.
   

• Select Show Navigator from the Commands menu.
  
• In the button module Explore, click the Navigator button.
  
• Enter the command Show-Navigator.
  

  Figure 181 : The Navigator. 
  -----
  (fig)  
         
  -----
  

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

Moving Up in the Behavior Tree

• In the Navigator, double-click the Up node, or select Up 1 from the pop-up menu available on the Up node.
  
• In the button module Explore, click the Up button.
  
• Enter the command Up 1.
  

• Enter the command Up, followed by the number of levels to move up.
  

• In the Navigator, select Up to top from the pop-up menu available on the Up node.
  
• In the button module Explore, click the Top button.
  
• Enter the command Top.
  

Moving Down in the Behavior Tree

To move one level down in the behavior tree, use one of the following methods:

• In the Navigator, double-click one of the Next nodes, or select Goto from the pop-up menu available on the Next nodes.
  
• Enter the command Next, followed by the number of the Next node, i.e. the number of the transition to execute.
  

• Enter the command Random-Down, followed by the number of levels to move down. For each level, a transition is chosen at random.
  

Moving Along the Current Path

The transitions making up the current path are labelled with three asterisks "***" in the nodes in the Navigator. However, no such marking is present when the transitions are listed with the List-Next command.

To move up along the current path, use the Up or Top commands as described in "Moving Up in the Behavior Tree" above.

To move one level down along the current path, use one of the following methods:

• In the Navigator, double-click the Next node labelled with three asterisks "***", or select Goto from the pop-up menu available on this node.
  
• In the button module Explore, click the Down button.
  
• Enter the command Down 1.
  

To move to the bottom of the current path, use one of the following methods:

• In the button module Explore, click the Bottom button.
  
• Enter the command Bottom.
  

Redefining the Current Root

In addition, you can at any time redefine the current root to either the current state or back to the system start state. To do this, enter the command Define-Root. Select or enter Current to redefine the current root to the current state. Select or enter Original to redefine the current root to the system start state.

Going to a System State

Using Manual Navigation

Returning to an Already Reached State

• Using Path Commands
  
• Using the Command Log
  
• Using MSC Trace.
  

The benefit of the MSC technique is that it is less vulnerable to changes in the state space options or in the SDL system. The drawback is that the exact same target state may not be reached. We only know that the path to the reached system state will satisfy the generated MSC trace.

Using Path Commands

1. When in the target state, enter the command Print-Path. The path from the root state to the current state is printed. The path is a sequence of integers indicating which transitions must be chosen to get to the current state.
   
2. At a later stage, enter the command Goto-Path, followed by the path printed above.
   

Using the Command Log

1. Before navigating to the target state, select Start Command Log from the Log menu, or enter the command Command-Log-On. Specify a file name on which all subsequent monitor commands will be stored.
   
2. Navigate to the target state.
   
3. Select Stop Command Log from the Log menu, or enter the command Command-Log-Off. The command logging is stopped and the file is closed.
   
4. Return to the same state in which the command log was started.
   
5. Execute the commands stored in the file by selecting Include Command Script from the Commands menu, or enter the command
   Include-File. Select or specify the earlier file name.
   

Using MSC Trace

1. When in the target state, generate an MSC trace from the root state to the current state. Enter the command MSC-Log-File, followed by a file name.
   
2. Return to the root state by using the Top command.
   
3. Go to the end of the MSC trace by verifying the MSC. See "Verifying an MSC" on page 411.
   

Using an MSC

Using a User-Defined Rule

To go to a target state using a user-defined rule:

1. Define the rule describing the target state (see "Managing User-Defined Rules" on page 427).
   
2. Define the report action for user-defined rules reports to be Abort (see "Report Action" on page 434). This will cause an automatic exploration to stop as soon as a state is reached that satisfies the rule.
   
3. Start an automatic state space exploration (see "Using a Default Exploration" on page 401).
   
4. Go to the state where the rule was satisfied and a report was generated (see "Going to a Report" on page 400).
   

Tracing, Logging and Viewing Facilities

Tracing the Execution

Textual Trace

• To print a textual trace for the transitions leading to the current state, enter the command Print-Trace, followed by the number of transitions to trace. That is, Print-Trace 1 prints the trace for the latest transition. The same information as for a full trace during simulation is printed.
  
• By default, the command Print-Trace 1 is executed in the Command window of the Validator UI, i.e., a continuous trace is in practice available in graphical mode.
  

Graphical SDL Trace

• To enable or disable continuous graphical trace, enter the command SDL-Trace. This command toggles the graphical trace; the current state of the trace is printed after the command is executed. When the trace first is enabled, an SDL Editor is opened as soon as the next transition is executed.
  
• In the Validator UI, the graphical trace can be controlled from the Commands menu. The command Toggle SDL Trace toggles the trace between enabled and disabled.
  

MSC Trace

• To enable or disable continuous MSC trace, enter the command MSC-Trace. This command toggles the trace; the current state of the trace is printed after the command is executed.
  
• In the Validator UI, the MSC trace can be controlled from the Commands menu. The command Toggle MSC Trace toggles the trace between enabled and disabled.
  

Before an MSC trace is started, you may define what types of events that will be traced. See "MSC Trace Options" on page 436 for more information.

Logging the User Interaction

Examining the System

There are, however, a few differences, due to the fact that there is no concept of the current scope in the Validator. This means that the View commands that in the Simulator operate on the current process instance work in a different way in the Validator. They require the process instance to be specified as the first parameter.

The available commands are shortly described below. See "Examining the System" on page 353 for more information.

• To list the process instances in the ready queue, enter the command List-Ready-Queue, or click the Ready Q button.
  
• To print overview information about process instances, enter the command List-Process, or click the Process List button.
  
• To examine a process instance, enter the command Examine-PId, or click the Process button. The process instance must be specified as the first parameter.
  
• To list all signal instances in the input port of a process instance, enter the command List-Input-Port, or click the Input Port button. The process instance must be specified as the first parameter.
  
• To examine a signal in the input port of a process instance, enter the command Examine-Signal-Instance, or click the Signal button. The process instance must be specified as the first parameter.
  
• To list all currently active timers, enter the command List-Timer, or click the Timer List button.
  
• To examine a timer instance, enter the command
  Examine-Timer-Instance, or click the Timer button.
  
• To examine a variable of a process instance, enter the command
  Examine-Variable, or click the Variable button. The process instance must be specified as the first parameter.
  

Performing Automatic State Space Explorations

In the Validator, 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.
  

• 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 most important monitor commands concerning state space explorations are available in the Explore module in the Validator UI.

Executing an Exploration

• 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).
  

  --------------------------------------------------------------------
  Note:                                                                 
  The button Verify MSC starts a bit state exploration, configured to   
  suite MSC verification. This is further described in "Verifying an    
  MSC" on page 411.                                                     
  --------------------------------------------------------------------
  

** 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

----------------------------------------------------------------
Note:                                                             
Depending on how an exploration is configured, it may take a con  
siderable amount of time to finish!                               
----------------------------------------------------------------

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

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

Rules Checked During Exploration

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" on page 426 for more information.

Interpreting Exploration Statistics

• No of reports: x
  The number of error situations found. How to investigate the reports are described in "Examining Reports" on page 398.
  
• 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" on page 431). 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" above.
  
• 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.
  

Examining Reports

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 182 : The Report Viewer. 
-----
(fig)  
       
-----

• 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 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

To show the whole report structure, select Expand Substructure from the pop-up 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

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.
   

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.
   

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

Validating an SDL System

Using a Default Exploration

To validate a system opened in the Validator:

1. If you already have executed commands for the opened validator, you should reset the validator. 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 Validator.
   
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" on page 396). 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" on page 396). 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" on page 398). 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 validator 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

• What was the symbol coverage reported in the statistics after the automatic exploration?
  
• Did the exploration finish by itself or was it stopped by the user?
  

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 validator options and start a new exploration (see "Using Advanced Validation" on page 404 and "Configuring the Validator" on page 429).
   
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

• The exploration was manually stopped before all symbols were reached.
  In this simple case, you should continue the exploration until it finishes by itself.
  
• The test values were inappropriate.
  Test values are used to define the set of possible signals from the environment. The automatically generated test values may not suite all SDL systems. This may for example cause the execution to never execute one branch of a decision statement. To overcome this problem, redefine the test values for the appropriate signal parameter. For more information on test values, see "Defining Signals from the Environment" on page 421.
  
• The exploration was pruned after a report.
  In most cases the Validator will prune the exploration of a particular path as soon as a report has been found, i.e., the exploration will not continue beneath the state in question. If you have examined such a report and has decided not to do anything about it, the Validator will still prune the search when it finds the report the next time. To overcome this problem, change the report action for this particular report type from prune to continue. See "Configuring the Validator" on page 429 for more information.
  
• Some parts of the system are, in fact, unreachable.
  If some parts of the SDL system are not reachable at all, it may be an indication that there is a design error in the system.
  
• There are problems with timer expirations.
  The validator is by default configured in a way that tries to reduce the size of the state space. It will always try to execute internal actions (e.g. tasks, decisions, internal input and outputs) before any timers are allowed to expire. The assumption is that the system will always execute fast enough to ensure that no timers will expire (the timers may of course expire when waiting for input from the environment). To make a more complete test of this type of situation, see "Using Advanced Validation" on page 404.
  
• The search depth was too small.
  The default search depth is 100. This may not be enough for some systems, e.g. a system with a very long initialization phase. In some cases, it is possible to overcome this problem simply by increasing the search depth (see "Configuring the Validator" on page 429). However, the techniques discussed in "Validating Large Systems" on page 405 are often more suitable.
  
• The state space is too big.
  Many SDL systems of reasonable complexity quite simply have state spaces that are too big; it is not possible to explore the entire state space in one exploration. Characteristic for this situation is a low symbol coverage, truncated paths, and either manually stopped exploration or a high (>10%) collision risk. This situation is discussed in "Validating Large Systems" on page 405.
  

Using Advanced Validation

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" on page 405 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" on page 410 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" on page 441 for information on which commands to use.

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

Validating Large Systems

The following techniques are discussed:

• Decomposed Exploration
  
• Using MSCs to Limit the Search
  
• Reducing the State Space Size
  
• Using Random Walk Exploration
  
• Incremental Validation.
  

Decomposed Exploration

The process of finding which and how many partial explorations that are necessary is a combination of an iterative process and a planning issue where the possible features and phases that can be subject to a partial exploration are identified. If an incremental design process is used it is often possible to use the different iterations to guide the choice of partial explorations; compare with "Incremental Validation" on page 411.

A common strategy used to find the needed partial explorations is essentially the following:

1. Start an exploration from the system start state.
   
2. Check all reports and correct the errors in the system. Generate a new validator and make another exploration.
   
3. When all found reports have been fixed, check the symbol coverage. If the coverage is 100%, the validation is finished; otherwise, continue with the next step.
   
4. Use the Coverage Viewer to check which parts of the SDL system that need more testing.
   
5. Go to a suitable system state and start a new exploration from there.
   
6. Repeat the process until the symbol coverage is 100%.
   

• Where to start each partial exploration.
  
• How to limit each partial exploration.
  

Where to Start a Partial Exploration

How to Limit a Partial Exploration

• The search depth
  
• The signals from the environment
  
• User-defined rules
  

By changing the list of signals that can be sent from the environment it is possible to control which parts of the system that will be exercised by an exploration. For example, if we are interested in testing the data transfer phase of a connection-oriented protocol specification, a good strategy would be the following:

• Go to a system state where the connection is established.
  
• Define the signals from environment to be only the signals relevant for the data transfer, and start the exploration. For a description of how to define and remove signals from the list of signals that can be sent from the environment, see "Defining Signals from the Environment" on page 421.
  

Using MSCs to Limit the Search

An MSC can be loaded to guide the search by using the command Load-MSC. Once an MSC is loaded, both interactive navigation in the state space, e.g. by using the Navigator, and automatic exploration will only search the parts of the state space that correspond to the loaded MSC.

This means that if you want to go back to normal exploration, you have to clear the loaded MSC by using the commands Clear-MSC or Reset.

------------------------------------------------------------------
Note:                                                               
The test values are not used at all when an MSC is loaded. All sig  
nals from the environment, including their parameter values, must   
be specified in the MSC.                                            
------------------------------------------------------------------

An MSC loaded into the Validator must comply with some requirements; see "Requirements for MSC Verification" on page 415.

Reducing the State Space Size

• The value of local variables
  
• The number of instances of process types
  
• The size of large data structures.
  

Local Variable Values

A user-defined rule (see "Using User-Defined Rules" on page 426) provides an efficient means to reduce the size of the state space by putting restrictions on variable values. In the example above a reasonable restriction might be that we only would like check what happens the first three times the variable is increased. A rule that expresses this is:

proc:1->var < 4;

Number of Process Instances

Size of Large Data Structures

• The size of the reachable state space increases extremely rapidly as the size of the data structure increases.
  
• The efficiency of the bit state algorithm is decreased as the size of system states increase. Essentially the time to compute a new system state is linear to the size of the system states.
  

Using Random Walk Exploration

The reason is that the random walk algorithm gives a possibility to get a partial exploration of the state space that is randomly chosen. Furthermore, the symbol coverage of the exploration is determined only by how long the exploration is allowed to run. The drawback with the algorithm is that if it is allowed to run for a long time, so that significant parts of the state space already have been covered, there is no mechanism to avoid that already explored paths are explored once more.

How to start a random walk exploration is described in "Executing an Exploration" on page 396. The random walk exploration algorithm is further described in "Random Walk Options" on page 432.

The best way to get an idea of what has been tested when using random walk is to use the Coverage Viewer to check the symbol coverage. Even if this is not the same as the coverage of the system state space, it will show if there are large portions of the system that have not been reached by the exploration.

Incremental Validation

First a number of state space explorations are executed with different start states, and perhaps different test values. Together these explorations should give a good process graph coverage of the SDL system representing the base functionality.

For each increment that is added, a number of additional explorations is performed that will cover the new features in the SDL system.

It is also probably worthwhile to define command scripts that automatically can execute the various explorations that should be run to achieve a good process graph coverage. This makes it possible to run all of the various explorations in an straight-forward way for each new increment that is added to the system.

Verifying an MSC

The first prerequisite for MSC verification is of course that we have an MSC that describes some desirable behavior that can be used to check the SDL system against. This MSC can be interactively created using the MSC Editor as part of a requirement analysis, but it is also possible to use MSCs created as execution traces in the SDT Simulator or the Validator itself as input to the MSC verification.

It is worth noticing that the MSC does not have to be a process level MSC. It is possible to use MSCs where the MSC instances correspond to SDL blocks and systems, and even mixed MSCs where some instances correspond to processes and other to blocks.

There are some requirements on MSCs to be used for MSC verification; see "Requirements for MSC Verification" on page 415.

The characteristics of the MSC verification algorithm is further described in "MSC Verification Options" on page 433.

Basic MSC Verification

1. If necessary, go to a system state that corresponds to the start of the MSC to verify. If the MSC describes events from the start of the system, go to the system start state. You may have to reset the validator first, especially if you already have an MSC loaded.
   
2. To start the MSC Verification, click the Verify MSC button in the Explore module, or enter the command Verify-MSC.
   
3. The MSC that you want to verify has to be specified. Either select it in the Standard File Selection Dialog that appears (in graphical mode), or enter the name of the file on the command line (in stand-alone mode).
   
4. A bit state exploration adapted to suite MSC verification is performed. After the exploration statistics, the result of the MSC verification is presented. If it was possible to find an execution trace that was consistent with the MSC, the text
   

** MSC <MSC name> verified **

** MSC <MSC name> NOT VERIFIED **

1. If the MSC was not verified, check the generated reports using the Report Viewer. There will be a number of "MSCViolation" reports. These reports identify the execution paths which violate the MSC, i.e., paths that contain events that are not part of the MSC. You may investigate these reports by using the method described in "Examining Reports" on page 398.
   
2. If the MSC was successfully verified, there will be a
   "MSCVerification" report (there may also be a number of
   "MSCViolation" reports, but they can be discarded). You do not have to go to this report; the Validator automatically goes to the state where the MSC was verified. This means that the current path is set up automatically.
   
3. To verify another MSC from the same start state, go to the top of the current path. It is now possible to directly start a new MSC verification, as described above (you do not have to reset the validator).
   

   -------------------------------------------------------------------------
   Note:                                                                      
   When MSC verification is started, the current root of the behavior         
   tree is redefined to the current state. This feature is used in the next   
   section, "Verifying a Combination of MSCs". (It also means that            
   you may have to reset the validator to be able to reach the system         
   start state again.)                                                        
   -------------------------------------------------------------------------
   

Verifying a Combination of MSCs

As an example, consider a situation where we have an MSC "Init" that will describe some initialization phase that is needed to set up the SDL system to some "idle" state from where two features are accessible. These features are described by the MSCs "f1" and "f2". If this would be a communication protocol, the "Init" might be a connection establishment, and "f1" and "f2" successful and unsuccessful data transfer.

To check these MSCs using the Validator, do like this:

1. Verify the MSC "Init". This will check the initialization and set up the current system state to the state where this MSC was satisfied, i.e., the "idle" state.
   
2. From this state, verify the MSC "f1". This will check the first feature and furthermore redefine the current root of the behavior tree to the current state, i.e., the state from where this MSC verification was started.
   
3. Go to the top of the current path. This will change the current state to the current root of the behavior tree, i.e., the state from where the verification of "f1" was started.
   
4. Verify the MSC "f2". This will check the second feature from the same state that the first feature was checked.
   
5. Reset the validator if you would like to start from the beginning again.
   

Using Batch MSC Verification

To accomplish this using the Validator the most efficient way is to use the command script facility in the Validator. A command script is simply a text file containing a number of Validator commands, usually one command per line. A command file can be loaded into the Validator by selecting Include Command Script from the Tools menu, or by entering the command Include-File.

Example 11 : Batch MSC Verification  

log-on msc.log
verify-msc init.msc
verify-msc f1.msc
top
verify-msc f2.msc
reset
verify-msc errorinit.msc
quit

Requirements for MSC Verification

• It must be possible to map each MSC instance to either the environment, the entire SDL system, a block, or a process. This mapping is done by matching the name of the MSC instance with the names of the corresponding SDL entities.
  
• All parameters to the MSC messages must be supplied.
  
• PId values are not allowed as parameters to MSC messages from the environment of the SDL system. PId values are allowed on internal messages and messages to the environment, but the values are not checked during the exploration
  
• If the MSC is on process level, only one static instance of each process type is allowed in the MSC. There is no limit to the number of dynamically created MSC instances.
  
• The MSC must not contain any coregions.
  

Using Observer Processes

To be useful, the observer processes must be able to inspect the SDL system without interfering with it and also generate reports that convey the success or failure of whatever they are checking.

To accomplish this, three features are included in the Validator:

• The observer process mechanism.
  By defining processes to be observer processes, the Validator will start to execute in a two-step fashion. First, the rest of the SDL system will execute one transition, and then all observer processes will execute one transition and check the new system state.
  
• The assert mechanism.
  The assert mechanism enables the observer processes to generate reports during state space exploration. These reports will show up in the list of generated reports in the Report Viewer. The details of the assertion mechanism is discussed in "Using Assertions" on page 428.
  
• The Access abstract data type.
  The purpose of the Access abstract data type is to give the observer processes a possibility to examine the internal states of the other processes in the system. Using the Access ADT it is possible to check variable values, contents of queues, etc., without any need to modify the observed processes. See "The Access Abstract Data Type" on page 417 for more details.
  

Figure 183 : A Simple Observer Process. 
-----
(fig)  
       
-----

Two characteristics for the observer processes are:

• the use of continuous signals with tests that use Access operator to check the internal state of other processes, and
  
• the use of assertions to report the result.
  

1. Create the observer processes in the SDL Editor. You should place the observer processes in a special block that you include in the diagram structure of the SDL system. In this block, you also need to specify an INCLUDE directive for the Access ADT:
   

/*#INCLUDE `access.pr' */

1. In the generated validator, define each observer process by using the command Define-Observer, followed by the name of the process type. All instances of the process type will now become observer processes.
   
2. Perform a state space exploration. If an assertion defined in an observer process is satisfied, an "Assertion" report is generated. To simplify the observer processes, an "Observer" report will also be generated whenever there is an observer process that cannot execute.
   

The Access Abstract Data Type

The Access ADT defines a number of SDL operators. The signatures of these operators are defined as follows;

  GetPID : CharString, integer -> PId;
    /* Returns the PId value of a process instance
       par 1: the name of the process type
       par 2: instance number of the process instance
    */
  GetState  : PId -> CharString;
    /* Returns the name of the current state of a
       process instance (or previous if the process is 
       not in a state)
       par 1: the pid of the process instance */
  GetNoOfInst: charstring -> integer;
    /* Returns the number of instances for a particular
       process type
       par 1: the name of the process type */
  terminated: PId -> boolean;
    /* Returns true if the process instance is
       terminated otherwise false
       par 1: The PId value of the process instance */
  GetProcedure: PId -> charstring;
    /* Returns the name of the procecure a process
       instance currently has called. If no procedure
       is called `none' is returned
       par 1: The PId value of the process instance */
  InProcedure: PId, CharString -> boolean;
    /* Returns true if a process instance currently 
       executes in a specific procedure, otherwise
       false
       par 1: The PId value of the process instance
       par 2: The name of the procedure */
  GetNoOfSignals: PID -> integer;
    /* Returns the number of signals currently in the
       input port of a process.
       par 1: The PId value of the process instance */
  GetSignalType: PId, integer -> charstring;
    /* Returns the name of the signal type for a
       signal in the input port of a process instance
       par 1: The PId value of the process instance.
       par 2: A number (>=1) identifying the signal */
  InQueue: PId, charstring -> boolean;
    /* Returns true if a process instance currently
       has a signal of a specific type in its input
       port queue
       par 1: The PId value of the process instance.
       par 2: The name of the signal type. */
  /* Variable access functions. These functions return
     a variable value that corresponds to one of the
     variables of a process instance as specified by
     the parameters.
       par 1: The PId value of the process instance.
       par 2: Variable name  */
        
  v : PId, charstring -> integer;
  vInteger : PId, charstring -> integer; 
  v : PId, charstring -> real; 
  vReal : PId, charstring -> real; 
  v : PId, charstring -> boolean; 
  vBoolean  : PId, charstring -> boolean; 
  v : PId, charstring -> Character; 
  vCharacter : PId, charstring -> Character;
  v : PId, charstring -> Time;
  vTime : PId, charstring -> Time;
  v : PId, charstring -> Duration;
  vDuration : PId, charstring -> Duration;
  v  : PId, charstring -> Charstring;
  vCharstring : PId, charstring -> Charstring;
  v : PId, charstring -> PId;
  vPId : PId, charstring -> PId;

P := GetPId( `Initiator', 1 ),
CS := GetState( P )

An example of a statement that will access the variable value for one of the variables of another process instance is:

LocalVar := v(P,'Var')

The operators for accessing the value of a variable are given in two versions for each predefined simple type: the v operator and the vXXX operator, where XXX is the name of the type. They are equivalent and the only time there is a need to use the vXXX operator is when it is not possible to resolve by context which of the v operators that is intended.

To access variables of sorts that are syntypes to the predefined simple types, the v operator for the corresponding predefined simple type can be used.

Accessing variable of structured types, enumeration types and user-defined types is a bit more complex. There are two possible ways to do it. Either define the v operator for the type in question, or use the #CODE operator and access the variable value using a C macro XVV.

Example 12 : Structured Types in Observer Processes  

  newtype MSDUType
    struct
      id IPDUType;
      num Sequencenumber;
      data ISDUType;
  endnewtype MSDUType;

newtype MSDUTypeAccess
literals NotUsedMSDUTypeAccess;
operators
  v /*#NAME `XVNAME(MSDUType)'*/ :
    PId, charstring -> MSDUType;
/*#ADT (H)
#TYPE
#define MSDUType #SDL(MSDUType)
*/
endnewtype MSDUTypeAccess;

LocalVar := v(P,'MSDUVar')!id

LocalVar := #CODE(`XVV(#SDL(P),"Var",#SDL(MyType))')

Defining Signals from the Environment

This is obviously a situation that is not acceptable when performing state space exploration. The SDT Validator allows three different strategies to avoid situations like this:

1. Create a closed system by specifying the environment of the system using SDL. This will solve the problem but introduces a new one; it is necessary to create an SDL model of the environment.
   
2. Specify the signals that can be sent from the environment to the system. This is a simple way to avoid the problem. By enumerating the signals with their parameters that the environment can send, a finite branching is guaranteed at each system state in the state space.
   
3. Use an MSC to guide the state space exploration. Since the MSC defines what signals the environment can send and their ordering, a limited part of the state space can be explored.
   

Test Values

Each time the Validator is in a state where input from the environment is possible during state space exploration, the list of signals defined by the test values is consulted.

The default test values for the predefined data types are:

-------------------------------
Data Type   Default Test Values  
-------------------------------
Integer     -55, 0, 55           
Boolean     true, false          
Real        -55, 0, 55           
Natural     0, 55                
Character   `a'                  
CharString  "test"               
Duration    0                    
Time        0                    
PId         Environment PId      
-------------------------------

• Enumerated types: All values in the type
  
• Subranges of the predefined data types: All values in the range
  
• Structures: All combinations of the test values of the individual fields
  
• Arrays: All combinations of the test values of the component type.
  

Test Values Restrictions and Options

• If the number of test values for a data type or signal parameter exceeds a maximum number, randomly chosen test values will be generated.
  
• If the number of signal instances for a particular signal type exceeds a maximum number, randomly chosen signal instances will be generated for this signal type.
  

• To define the maximum number of test values for any data type or signal parameter, enter the command Define-Max-Test-Values, followed by the number of test values. The default is 10.
  
• To define the maximum number of signal instances for any signal type, enter the command Define-Max-Signal-Definitions, followed by the number of signal instances. The default is 10.
  

  ----------------------------------------------------------------------
  Note:                                                                   
  These options affect the state space; see "Affecting the State Space"   
  on page 430.                                                            
  ----------------------------------------------------------------------
  

Defining and Listing Test Values

Changing the test values are therefore only needed if you would like to fine-tune the behavior of the Validator, or if the signals from the environment have parameters that are of a user-defined or unusual data type.

-----------------------------------------------------------------------
Note:                                                                    
Changing test values affects the state space; see "Affecting the State   
Space" on page 430.                                                      
-----------------------------------------------------------------------

The monitor commands concerning test values are available in the Test Values module in the Validator UI.

Test Values for Data Types

• To define a new test value for a sort, enter the command
  Define-Test-Value, or click the Def Value button. The parameters are the sort and the value. Example:
  

Define-Test-Value integer 20

• To list the new test values defined for all sorts, enter the command List-Test-Values, or click the List Value button.
  
• To clear all test values for a sort, enter the command
  Clear-Test-Values, or click the Clear Value button. As parameter, you either specify the sort, or `-' which means all sorts.
  

Test Values for Signal Parameters

• To define a new test value for a signal parameter, enter the command Define-Parameter-Test-Value, or click the Def Par button. The parameters are the signal, the ordinal number of the signal parameter, and the value. Example:
  

Define-Parameter-Test-Value Score 1 -5

• To list the new test values defined for all signal parameters, enter the command List-Parameter-Test-Values, or click the List Par button.
  
• To clear all test values for a signal parameter, enter the command
  Clear-Parameter-Test-Values, or click the Clear Par button. As parameter, you specify the signal and the ordinal number of the signal parameter. You may use `-' for the parameter number, which means all signal parameters, or just `-' for the signal, which means all signal parameters for all signals.
  

Test Values for Signal Instances

• To define a new set of test values for a signal instance, enter the command Define-Signal, or click the Def Signal button. The parameters are the signal and an optional set of values for the parameters. Multiple Define-Signal commands may be used to define several signal instances of the same signal type, but with different values. Example:
  

Define-Signal Test 10 'hello' true
Define-Signal Test -5 'bye'
----------------------------------------------------------------------------
Note:                                                                         
The signals defined using this command are cleared when the signal            
list is regenerated, e.g. if a test value is defined for a sort or a signal   
parameter.                                                                    
----------------------------------------------------------------------------

• To list all currently defined signal instances, enter the command List-Signal-Definitions, or click the List Signal button.
  
• To clear all test values for a signal type, enter the command
  Clear-Signal-Definitions, or click the Clear Signal button. As parameter, you specify the signal, or `-' which means all signals.
  

Saving Test Values

To save the test values, enter the command Save-Test-Values, followed by a file name. To read in the saved test values again, enter the command Include-File, followed by the file name.

Using User-Defined Rules

Different Usages

• To verify properties of the SDL system.
  A user-defined rule describes properties of system states. By using an automatic state space exploration, it is thus possible to verify the existence of system states that satisfy the specified properties. If the state space is small enough to allow a complete exploration it is also possible to verify that the state space does not contain any system state with the specified property.
  
• To search for specific system states.
  A user-defined rule makes it possible to go to a specific system state in the state space without the need to use the navigating commands of the validator monitor. By describing the desired state with a rule and using an automatic state space exploration, you can go directly to the report that satisfied the rule. In this case, the report action for the user-defined rule report should be set to Abort.
  
• To reduce the state space to be explored.
  For many SDL systems, the state space can be very large or even infinite, which makes it difficult to perform a state space exploration effectively. However, in many cases the state space contains large subspaces that for some reason are not interesting to explore. For instance, they may be equivalent to other parts of the state space except for the value of one particular variable. In such cases, a user-defined rule can be used to restrict the exploration by defining system states that are considered to be uninteresting. When such a state is encountered, the exploration is truncated and continued in another node.
  

Examples of Rules

exists P:Proc | P->var=12;

A simple example of a rule that searches for a system state is:

state(initiator:1)=disconnected;

A more complex example of such a rule is:

state(Game:1)=Winning and 
sitype(signal(Game:1))=Probe

An example of a rule that reduces the state space is:

(Game:1->Count > 2) or (Game:1->Count < -2)

For a full description of the features and syntax of user-defined rules, see "User-Defined Rules" on page 1940.

Managing User-Defined Rules

To clear the user-defined rule, enter the command Clear-Rule.

To print the definition of the current user-defined rule, enter the command Print-Rule.

To evaluate the user-defined rule in the current system state, i.e. to check whether the rule is satisfied, enter the command Evaluate-Rule.

Using Assertions

Example 13 : Assertion in C Code  
TASK '' /*#CODE
#ifdef XASSERT
  if (#(I) < #(K))
    xAssertError("I is less than K");
#endif
*/ ;
  

The xAssertError function, which has the following prototype:

extern void xAssertError ( char *Descr )

Configuring the Validator

Managing Options

If the options are changed during a session with the Validator, you will be asked whether to save the options when you exit or restart the currently executing validator. If you save the options, the new values will be stored in a file named .valinit in the directory from where SDT was started. This file will automatically be loaded the next time the Validator is started from the same directory, thus restoring the previous options.

Some monitor commands operate on all the options:

• To print a list of all options and their current values, select
  Show Options from either the Options1 or Options2 menu, or enter the command Show-Options. (A few of the options described here are not listed.)
  
• To set all options to their predefined default values, click the
  Default button in the Explore module, or enter the command
  Default-Options. Note that this also clears all reports.
  
• To set all options to their initial values, i.e. the values set when the validator was started, click the Reset button in the Explore module, or enter the command Reset.
  

  ------------------------------------------------------------------
  Note:                                                               
  This command also resets the validator completely and is equiv      
  alent to restarting the validator from scratch. To just set the op  
  tions to their initial values without resetting the validator:      
  1.  Set the options to their default values. See above.             
  2.  Read in the .valinit file (see above). Select 
  
                   
  Include Command Script from the Commands menu, or enter the         
  command Include-File.                                               
  ------------------------------------------------------------------
  

Affecting the State Space

In this case, the following dialog is opened:

Figure 184 : Changing the Current Root. 
-----
(fig)  
       
-----

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

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:

• If both of the positions indicated by the hash values are already set, the state is considered to have been previously visited. The search of this particular path in the state space is pruned, and the search backs up to a previous system state and continues elsewhere.
  
• If both of the positions are not set, the state is a new state that has not been previously visited. Both position in the bit array are then set and the search continues with the successor states.
  

Search Depth

• Default value: 100
  
• Command: Define-Bit-State-Depth
  
• Menu choice: Options2: Bit-State: Depth
  

Hash Table Size

• Default value: 1,000,000 (bytes)
  
• Command: Define-Bit-State-Hash-Table-Size
  
• Menu choice: Options2: Bit-State: Hash Size
  

Random Walk Options

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

• Default value: 100
  
• Command: Define-Random-Walk-Depth
  
• Menu choice: Options2: Random: Depth
  

Repetitions

• Default value: 100
  
• Command: Define-Random-Walk-Repetitions
  
• Menu choice: Options2: Random: Repetitions
  

Exhaustive Exploration Options

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

• Default value: 100
  
• Command: Define-Exhaustive-Depth
  
• Menu choice: Options2: Exhaustive: Depth
  

MSC Verification Options

• An MSC is always loaded to guide the search
  
• The search depth is different from the depth used during usual bit state exploration
  
• The search is aborted as soon as the MSC has been verified.
  

Search Depth

• Default value: 1,000
  
• Command: Define-MSC-Verification-Depth
  
• Menu choice: Not available
  

Timer Check Level

• 0: No checking of timer events is performed.
  
• 1: If a timer event exists in the MSC a matching timer event must exist in the explored SDL path, but a timer event in the explored SDL path is accepted even if there is no corresponding MSC timer event.
  
• 2: All timer events in the MSC must match a corresponding timer event in the explored SDL path, and vice versa.
  

This option affects the state space; see "Affecting the State Space" on page 430.

• Default value: 1
  
• Command: Define-Timer-Check-Level
  
• Menu choice: Options2: MSC: Timer check level
  

Report Options

Report Action

• Continue: The search continues past the reported situation as if it never happened.
  
• Prune: The search is pruned and depending on the algorithm some appropriate action is taken. For example, when using bit state exploration, the search will back up one state and continue with the next alternative transition, as if max search depth was reached and the search truncated.
  
• Abort: The search is aborted and the command prompt displayed.
  

This option affects the state space; see "Affecting the State Space" on page 430.

• Default value: Prune for all report types
  
• Commands: Define-Report-Continue, Define-Report-Prune and Define-Report-Abort
  
• Menu choices: Options2: Report: Continue, Options2: Report: Prune and Options2: Report: Abort
  

Report Log

This option affects the state space; see "Affecting the State Space" on page 430.

• Default value: On for all report types
  
• Command: Define-Report-Log
  
• Menu choice: Options2: Report: Report log
  

Report Viewer Autopopup

• Default value: On
  
• Command: Define-Report-Viewer-AutoPopup
  
• Menu choice: Options1: Report Viewer Auto Popup
  

MSC Trace Options

Action Trace

• Default value: Off
  
• Command: Define-MSC-Trace-Action
  
• Menu choice: Not available
  

State Trace

• Default value: On
  
• Command: Define-MSC-Trace-State
  
• Menu choice: Not available
  

MSC Trace Autopopup

• Default value: On
  
• Command: Define-MSC-Trace-Autopopup
  
• Menu choice: Options1: MSC Trace Auto Popup
  

State Space Options

Since these options affect the state space, note the information in "Affecting the State Space" on page 430.

Transition Type

• It can be equal to a complete SDL process graph transition (the value "SDL" in the command)
  
• It can be a part of such an SDL transition (the value
  "Symbol-Sequence" in the command).
  

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.

• Default value: SDL
  
• Command: Define-Transition
  
• Menu choice: Options1: State Space: Transition
  

Scheduling Algorithm

• All of the process instances in the ready queue are allowed to execute (the value "All" in the command)
  
• Only the first process instance in the ready queue is allowed to execute (the value "First" in the command).
  

If all process instances are allowed to execute, the semantics of ITU recommendation Z.100 are modelled. 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 SDT Code Generator are modelled. There will only be one child node to the current node in the behavior tree, the first process instance in the ready queue.

• Default value: First
  
• Command: Define-Scheduling
  
• Menu choice: Options1: State Space: Scheduling
  

Event Priorities

• Internal events: Events local to the processes in the system, e.g., tasks, decisions, inputs, outputs.
  
• Input from ENV: Reception of signals from the environment. The signal is put in the input port of a process instance or on a channel queue.
  
• Timeout events: Expiration of SDL timers. The timer signal is put in the input port of a process instance.
  
• Channel outputs: A signal is removed from a channel queue and put into another channel queue or the input port of a process instance
  
• Spontaneous transitions: A transition in a process caused by input of none.
  

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

• All event classes are assigned priority 1.
  
• Internal events and channel outputs are assigned priority 1, and external, timeout and spontaneous transition events are assigned priority 2 (the default).
  

• Default value: Priorities 1, 2, 2, 1, 2
  
• Command: Define-Priorities
  
• Menu choice: Options1: State Space: Priorities
  

Channel Queues

• Default: No channels have queues
  
• Command: Define-Channel-Queue
  
• Menu choice: Options1: State Space: Channel queues
  

Maximum Input Port Length

• Default value: 3
  
• Command: Define-Max-Input-Port-Length
  
• Menu choice: Options1: State Space: Input port length
  

Maximum Transition Length

• Default value: 1,000
  
• Command: Define-Max-Transition-Length
  
• Menu choice: Options1: State Space: Transition length
  

Maximum Number of Instances

• Default value: 100
  
• Command: Define-Max-Instance
  
• Menu choice: Options1: State Space: Max instance
  

Maximum State Size

• Default value: 100,000 (bytes)
  
• Command: Define-Max-State-Size
  
• Menu choice: Options1: State Space: Max state size
  

Timer Progress

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" on page 1937.

• Default: On (timer expiration is considered to be progress)
  
• Command: Define-Timer-Progress
  
• Menu choice: Options1: State Space: Timer progress
  

Spontaneous Transition Progress

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

• Default: On (spontaneous transition is considered to be progress)
  
• Command: Define-Spontaneous-Transition-Progress
  
• Menu choice: Not available
  

Setting Advanced Options

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 scheduling should be set to All, since we in this case are looking for signal races and a characteristic property of signal race conditions is that they are depending on the ordering of internal events.
  
• The priorities should be set to 1 for all types of events.
  
• To reduce the size of the state space, the maximum queue length should be set to a very small number. The reason is that when the environment is allowed to send signals to the system at any time, the queues that can receive signals from the environment will grow very rapidly.
  
• Since a lot of maximum queue length reports will be generated with these options, the report log for this report should be set to Off. Note also that the report action for this report should be Prune (which is the default).
  

References

[1]

Holzmann, G.J:
Design and Validation of Computer Protocols
Prentice-Hall, 1991
ISBN 0-13-539834-7

Table of Contents

Next Chapter