Alternatively, click the Open quick button in the tool bar.
This chapters provides general information related to validation in SDT and describes the actions you perform when validating an SDL system.
For a reference to the validator user interface, see The SDT Validator.
How to use Autolink, a part of the SDT Validator, is described in Using Autolink.
The Validator is a tool intended to support engineers involved in development of specifications or designs using SDL. It is designed to give the engineers a possibility to increase the quality of their work and to automate time-consuming tasks. It is focused on the following major application areas in the development process:
An executable validator is built up in the same way as a simulator. See Structure of a Simulator for more information.
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.
The SDT Validator 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 [15], see References.
The SDT Validator 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 Validator is configured.
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.
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.
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.
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 crated 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 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.
There are two ways to generate and start a validator:
In the following, the more complex way will be described first, to give a full understanding of the process. The quick way is described in Quick Start of a Validator.
The Validator is implemented as a precompiled run-time kernel to the SDT C Code Generator in the same way the SDT Simulator is implemented. To start a Validator for an SDL system, or a part of an SDL system, it is thus necessary to first generate an executable validator. This is done from the Organizer.
To generate an executable validator:
<system>_xxx.val (on UNIX), or <system>_xxx.exe (in Windows), where the _xxx suffix is platform or kernel/compiler specific. The Status Bar of the Organizer reports the progress of the generation; the last message should be "Compiler done."An executable validator can be run in two different modes; graphical mode and stand-alone mode (textual mode).
In graphical mode, the Validator takes advantage of SDT's graphical user interface and integration mechanism. A separate graphical user interface, the Validator UI, is started, giving access to the monitor system through the use of menus, command buttons, etc.
To start a validator in graphical mode:
A welcome message is printed in the text area of the Validator UI. The monitor system is now ready to accept commands. Please see Supplying Values of External Synonyms for some additional information that may affect the start-up.
In stand-alone mode, the Validator uses the input and output devices currently defined on your computer, which provide a textual, command-line based user interface. A very limited graphical support is provided when running the Validator in this 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
A welcome message is printed on the terminal:
Welcome to SDT VALIDATOR Command :
The monitor system is now ready to accept commands. Please see Supplying Values of External Synonyms for some additional information that may affect the start-up.
A validator can also be generated and automatically started in graphical mode in one single step.
To quick start a validator, click the Validate quick button in the Organizer's tool bar. The following things happen:
It is possible to start a validator for a part of an SDL system (a block or a process) by selecting the block/process and then clicking on the Validate button.
An executing validator can be restarted from the beginning to reset its state completely:
The SDL system for the validator may contain external synonyms that do not have a corresponding macro definition (see External Synonyms). In that case, you will be asked to supply the values of these synonyms, either by selecting a file with synonym definitions or by entering each synonym value from the keyboard.
In stand-alone mode, the following prompt appears:
External synonym file :
Enter the name of a file containing synonym definitions, or press <Return> to be prompted for each synonym value.
In graphical mode, a file selection dialog is opened. Either select a file (*.syn) containing synonym definitions, or press Cancel to be prompted for each value in a separate dialog. In this dialog, the name and type of the synonym is shown together with an input text field. You can now do one of the following:
If a synonym file is selected in the file selection dialog, this file is also used when the validator is restarted. (If you by any chance want to use another synonym file you have to start a new Validator UI.)
If you set the environment variable SDTEXTSYNFILE to a file before starting SDT this file will automatically be used. If SDTEXTSYNFILE is set to "[[" all synonyms are given "null" values.
The syntax of a synonym file is described in Reading Values at Program Start up.
When a validator is started, the static process instances in the system are created, but their initial transitions are not executed.
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 for more information.
Monitor commands in the Validator are issued in the same way as in the Simulator, since the same monitor system is used in both tools. Also, the Validator UI works in the same way as the Simulator UI. Please see Issuing Monitor Commands for more information.
The Validator UI can be customized in the same way as the Simulator UI. Please see Customizing the Simulator UI for more information.
However, there are a few differences between the user interface of the Validator and the Simulator. These differences are described below.
The validator's monitor system becomes active when the validator is started, when a transition executed during navigation has completed, when an automatic state space exploration has finished, when a report with Abort action has been generated, or when an automatic state space exploration is manually stopped.
These conditions are listed in greater detail in Activating the Monitor.
The graphical Validator UI is illustrated in the figure below:
|
|
Since the set of available commands differ between the Simulator UI and the Validator UI, the set of button modules and command buttons is also different. In addition, three extra menus are available in the menu bar: Commands Menu, Options1 Menu and Options2 Menu. The menu choices in these menus are similar to the command buttons in the sense that each of them correspond to a certain monitor command.
The Command and Watch windows are also available in the Validator UI. The difference compared to the Simulator UI is:
The SDT Validator provides the possibility to interactively walk around in the behavior tree of an SDL system. This is also known as manually navigating in the state space. A dedicated graphical tool, the Navigator, is available in the Validator to facilitate manual navigating. However, it is possible to use manual navigation without using the Navigator tool.
The Navigator is intended to be used in three different situations:
To open the Navigator tool, use one of the following methods:
|
|
The boxes shown in the Navigator represent the behavior tree transitions leading to and from the current system state. They are labelled
Up 1 (for the transition leading to the current state) and Next 1, Next 2, etc. (for the transitions leading from the current state).
To close the Navigator, click the Close quick button in the tool bar.
To move one level up in the behavior tree, use one of the following methods:
To move more than one level up in the behavior tree at once:
To move to the current root of the behavior tree, i.e. the top of the current path, use one of the following methods:
To see the possible Next nodes when the Navigator is not opened, enter the command List-Next. This gives a numbered list of all transitions leading from the current state.
To move one level down in the behavior tree, use one of the following methods:
To move more than one level down in the behavior tree at once:
The current path can be seen as the path in the behavior tree that has been explored last. It is set up when going to a report (see Going to a Report) and when interactively walking down the behavior tree.
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:
To move more than one level down along the current path at once, enter the command Down, followed by the number of levels to move down.
To move to the bottom of the current path, use one of the following methods:
The current root of the behavior tree is initially set up to the system start state. The current root is automatically redefined to the current state when using MSC verification (see Verifying an MSC). It can also be redefined as an effect of changing validator options (see Affecting the State Space).
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.
When using the Validator it is quite common that there is a need to go to a specific system state, for instance to be able to start an automatic state space exploration from this point. This section describe some possibilities to in an efficient way get to the wanted system state, called the target state below.
In many cases the simplest way is to use the Navigator tool or the navigation commands to interactively traverse the path to the target state. Manual navigation is described in Navigating in the State Space.
It is possible to return to a state that has been reached in an earlier stage when using the Validator. Three methods will be discussed:
The benefit of the first two techniques is that the exact same target state will be reached. The drawback is that these techniques will not work as soon as either the SDL system or the state space options have been changed (see State Space Options).
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.
To go to the target state using path commands:
To go to the target state using the command log:
To go to the target state using MSC trace:
If an MSC is created that describes the events leading to the target state, verifying this MSC gives a possibility to go to a system state that satisfies the MSC in an efficient way. It does not matter if the MSC is manually created, generated from the Simulator or from the Validator itself (as discussed in Using MSC Trace, above). However, the exact same target state may not be reached by this method. We only know that the path to the reached system state will satisfy the generated MSC trace.
If the target state can be described in terms of process states, variable values, etc., a convenient way to get to a state that satisfies the description is to use a user-defined rule (see Using User-Defined Rules).
To go to a target state using a user-defined rule:
The benefit with this method is that it is fast and efficient, especially if the target state is on a considerable depth in the state space. The drawback is that sometimes there are shorter paths to the target state than the one that was automatically generated.
In the Validator, the same kind of commands as in the Simulator are available for tracing the execution, logging the user interaction and examining the system. There are a few differences, described below.
In the Validator, the same type of printed trace information is available for executed transitions as in the Simulator; see Textual Trace. Unlike the Simulator, however, there is no command to start continuously printing the textual trace; instead, a command must be explicitly used whenever a trace is wanted.
Graphical trace of SDL symbols in the source GR diagrams is available. The graphical trace in the Validator selects all symbols that were executed in the transition leading to the current state. This is different from the Simulator, where GR trace selects the next symbol to be executed.
MSC trace enables tracing of executed events in an MSC Editor. When the trace first is enabled, an MSC Editor is opened, showing the events executed up until the current state, and the current path is set up. After that, the trace is continuously updated in the MSC Editor as transitions are executed. This means that events are added when you navigate down the behavior tree, the selected event is changed when you navigate up, and the MSC is redrawn when you move outside the current path.
The MSC trace from the current root to the current state can also be saved on a log file, which later may be opened from an MSC Editor. To save such an MSC log, enter the command MSC-Log-File, followed by the file name. The MSC log file should be given the file extension .mpr.
Before an MSC trace is started, you may define what types of events that will be traced. See MSC Trace Options for more information.
The interaction between the user and the Validator can be logged on file in exactly the same way as in the Simulator. See Logging the User Interaction for more information.
The current state of the system can be examined in the same way as in the Simulator. The View commands available in the View module of the Validator UI are generally the same ones as in the View module of the Simulator UI.
Some of the commands used for examining the system operate on a specific process instance, the current process, identified by the current scope. A scope is a reference to a process instance, a reference to a service instance if the process contains services, and possibly a reference to a procedure instance called from this process/service (the current procedure).
The scope is automatically set by the validator to the process instance that executed in the transition leading to the current system state. You may change the scope if you would like to examine another process, service or procedure instance.
The available commands are shortly described below. See Examining the System for more information.
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 Validator, three types of automatic state space explorations can be used, implemented as different algorithms:
The characteristics of these algorithms are further described in Configuring the Validator. They have the following in common:
The performance and results of a state space exploration are also highly dependent on how the state space is configured. This is discussed in State Space Options.
The most important monitor commands concerning state space explorations are available in the Explore module in the Validator UI.
The different types of explorations are started in the following way:
|
Note: The button Verify MSC starts a bit state exploration, configured to suit MSC verification. This is further described in Verifying an MSC. |
When the exploration is started, a message is printed stating the options used for this exploration type (see Configuring the Validator):
** Starting bit state exploration ** Search depth : 100 Hash table size : 1000000 bytes ** Starting exhaustive exploration ** Search depth : 100 ** Starting random walk ** Depth : 100 Repetitions : 100
By default, the exploration continues until it is finished, i.e., until the state space has been fully explored according to the exploration options. During the exploration, a status message is repeatedly printed after a certain number of transitions or states have been generated.
|
Note: Depending on how an exploration is configured, it may take a considerable amount of time to finish! |
To stop an exploration manually, click the Break button in the Validator 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 Validator always returns to the start state of the exploration when it is finished or stopped.
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.
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.
When an exploration has been performed, the reported error situations should be examined. A dedicated graphical tool, the Report Viewer, is available in the Validator to facilitate the report examination. However, it is possible to examine the reports without using the Report Viewer.
The Report Viewer is by default automatically opened when an exploration has been performed. To open the Report Viewer manually, either select Show Report Viewer from the Commands menu, or enter the command Show-Report-Viewer.
Figure 472 : The Report Viewer
|
|
The nodes in the Report Viewer are structured in three levels and show, from top to bottom:
To close the Report Viewer, click the Close quick button in the tool bar.
To list the reports when the Report Viewer is not opened, enter the command List-Reports, which prints a numbered list of all reports.
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.
When "going to a report," the Validator 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:
To go to a report using monitor commands:
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.
This section describes how to use the automatic state space exploration facilities in the Validator to look for inconsistencies and design errors in an SDL system. The idea is essentially to test the robustness of the application, the responses to unexpected situations. Essentially the validation is an attempt to answer questions like:
...and all other questions the designer never ever would imagine.
It is assumed that the SDL system is of moderate size and complexity; techniques for validating large SDL systems are described in Validating Large Systems.
When you are to use the Validator to try finding errors in a new SDL system for the first time, you are advised to start a bit state exploration using the default options.
To validate a system opened in the Validator:
When all reports have been checked and the found errors possibly have been corrected, the next question arises: When are we finished validating the system? To answer this question, look at these aspects:
The following possibilities now exist:
If the symbol coverage after an exploration is 100%, all parts of the system have been executed at least once. If the symbol coverage is less than 100%, the possible reasons why parts of the state space have not been reached are listed below.
To find out which parts of the system that have not been reached, a tool called the Coverage Viewer is used. To start the Coverage Viewer, select Show Coverage Viewer from the Commands menu, or enter the command Show-Coverage-Viewer. If the symbol coverage was less than 100%, the Coverage Viewer will display a tree structure representing the parts of the system that have not been executed.
The default options for the state space exploration, in particular the options that define the structure of the state space, are optimized to give good results for a first validation of a system. They are intended first of all to test for internal inconsistencies in the SDL system and to get a good process graph coverage. This assumes a reasonably "nice" environment, i.e., the environment only sends signals when nothing can happen internally in the system.
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 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 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 for information on which commands to use.
For a more in-depth explanation of the state space options, see State Space Options.
This section discusses various techniques that are useful when designing and validating large SDL systems. A large system is, in this context, a system that has a state space that is too large to be completely explored using one automatic state space exploration. The techniques are pragmatic and intended to give a reasonable chance of finding any errors even though the complete state space is not searched.
The following techniques are discussed:
The idea when using decomposed explorations is to use a number of reasonably small explorations instead of one big exploration. Quite often the behavior of an SDL system can be divided into a number of "phases" or "features." The idea is to explore each of these phases or features separately. The benefit with this approach is that it is a lot easier to explore the different phases separately than trying to explore the combination of all phases. The drawback is that errors that are caused by an interaction between different phases or features are not found. However, for large SDL systems it is sometimes the only possible method that at least can give a complete symbol coverage.
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.
A common strategy used to find the needed partial explorations is essentially the following:
There are two issues of this strategy:
The problem of identifying where to start a new exploration is of course system dependent and requires knowledge of the SDL system. The tool to use in this case is the Coverage Viewer, which shows exactly what parts of the SDL system that have been executed during the exploration and what parts have not been executed. Once a system state has been chosen the next issue is how to get there in the Validator. There are number of possible ways to do this; see Going to a System State.
The next problem is to limit each partial exploration to the intended part of the state space. There exists a number of factors which can be used to influence the extent of an exploration:
The search depth is the simplest limiting factor to use. By reducing the search depth, e.g. to 10 or 20, the size of the exploration will of course be considerably reduced compared to the default depth of 100.
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:
User-defined rules also give a possibility to limit the extent of an exploration. Define a rule that matches the system states where the exploration should be pruned and check that the report action for user-defined rules is to prune the search. For example, the rule would prune the exploration whenever the initiator process entered the state Idle. User-defined rules are described in Using User-Defined Rules.
state(initiator:1)=idle
Another possibility that sometimes is useful to control the exploration of the state space is to use MSCs to guide the exploration. This is particularly useful for SDL systems with a design that uses restrictions on the possible behavior of the environment of the system. It might, for example, be known that the signals A, B and C always will come in this order from the environment of the system. In this case it is not interesting to analyze what will happen if the signals will come in a different order.
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 how the test values are used when an MSC is loaded. It is allowed to leave out parameters to messages in the MSC. If a parameter is left out on a signal from the environment, the test values are used to determine the parameter values that are actually sent to the system. This is a useful feature when using MSCs to limit the search. See section Verifying an MSC for more details.
Another useful hint when using MSCs is to always use system level MSCs to guide the state space exploration. A system level MSC will allow a larger part of the state space to be explored than a block or process level MSC.
An MSC loaded into the Validator must comply with some requirements; see Requirements for MSC Verification.
The bit-state search uses a hash value based algorithm to store the state space that is traversed. Unfortunately the computation of hash values from a system state is an expensive operation and most of the execution time in a bit-state search is spent calculating hash values. The execution time for the hash algorithm is in most situations proportional to the size of each system state. The max and min system state size used by the hash algorithm is included in the statistics printed after each bit state search and should be checked if the search is slow. (See Bit-State-Exploration).
If the size of a system state is big (> 10,000 bytes) the bit state execution of the validator will be fairly slow. In these cases it might be worthwhile to try to optimize the performance by reducing the state size that the validator uses when computing hash values. This can be done by informing the validator to skip a number of variables when computing hash values. The validator includes a command Define-Variable-Mode that is intended for this purpose. (See Define-Variable-Mode.) For example the command:
define-variable-mode monitor subscrTab skip
will make the validator skip all subscrTab variables in monitor processes.
A typical example of where this feature is useful is if the system includes a big array (or other big data structure) that is initialized at the start up of the system and that after the initialization is known to be constant in the part of the state space that is explored. The correct way to take advantage of this in the validator is to:
Using this strategy it is possible to considerably increase the performance of the validator.
Another situation where the variable mode can be changed to "Skip" is when there are variables in the system that is known not to have any influence on the dynamic behavior of the system. See Variables Not Influencing the Dynamic Behavior.
There is a number of ways to reduce the state space that is necessary to explore by using knowledge and assumptions about the SDL system. Usually this is based on the fact that the state space of an SDL system contains various "sub state spaces" that are equivalent except for some detail, which is not very interesting for the purpose of the validation. Some examples of such details are:
An example of the way local variable values influence the size of the state space is the following: Consider a situation where a process contains an integer variable that counts the number of times a particular signal comes from the environment, and then replies with this number when requested to do so from the environment. It is obviously not especially interesting to try to investigate the behavior of the SDL system for all possible values of this local variable. Instead a reasonable set of values should be selected and the state space exploration guided by this selection.
A user-defined rule (see Using User-Defined Rules) 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;
Once this rule is defined and the report action for user-defined rule violation is set to Prune (which is the default), only the interesting parts of the state space are explored.
Another issue is the number of process instances that are used for each process type. If the number is large and all of them do the same thing, for example by modeling different connections in a connection oriented protocol, it is probably not very useful to try to explore the combination of all instances. Instead, it is better to restrict the number of instances allowed in the exploration. This can be achieved with the command Define-Max-Instance (see Maximum Number of Instances). If preferred, it is also possible to use a user-defined rule or an observer process to achieve the same result.
A third area where the validator performance is reduced is when large data structures, e.g. arrays, are used in the SDL system. A large data structure has two unfavorable effects on a state space exploration:
A good idea in this context is to, whenever possible, try to reduce the size of any large data structures in the SDL system before performing validation. Another possibility is to skip the variable when computing hash values as described in More Efficient Bit-State Exploration.
In many situations an SDL system contains a number of variables that does not have any impact on the dynamic behavior of the system. Essentially all variables that does not (directly or indirectly) have any influence on the path taken through a decision or the expression used when computing the receiver of a signal in output/RPC call will not influence the dynamic behavior of the system.
These variables can safely be ignored when performing a state space search. This can be accomplished by instructing the validator to skip these variables using the Define-Variable-Mode command. (See Define-Variable-Mode.) This will in many cases drastically reduce the size of the state space that the validator needs to search and is an efficient way to improve the performance of the validator.
Note that implicit variables like Sender/Parent/Offspring are also considered as variables in this respect. In particular Sender can be of interest to skip if it is not used, since it may change value every time a signal is received.
As an example, if Sender is not used in a process `p' the following command will make the validator ignore the Sender implicit variable when comparing two system states:
define-variable-mode p Sender skip
In some situations it is not possible to use the more elaborated techniques described in this section to cope with the problem of validating large SDL systems. The time and resources available for the validation may simply be too limited. A possible strategy to use when validating very large SDL systems is to use the random walk exploration strategy instead of the bit state algorithm.
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. The random walk exploration algorithm is further described in Random Walk Options.
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.
A common way to develop large SDL specifications and designs in practice is to use an incremental development strategy. First a base functionality is implemented and then various features are added in an incremental fashion. When this type of development process is used, a good way to plan the validation of the system is to let the different increments define the state space explorations that should be performed.
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.
MSC verification is one the major application areas for the SDT Validator. This section describes how to use the Validator to get started with MSC verification. It also gives some ideas of how to organize MSCs to be able to use common initialization MSCs and shows how to use batch files to achieve an efficient regression testing of an SDL system using MSC verification.
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.
The characteristics of the MSC verification algorithm is further described in MSC Verification Options.
To verify an MSC for a system opened in the Validator:
** MSC <MSC name> verified **is printed, where <MSC name> is the name of the MSC that was checked. If it was not possible to find a consistent execution trace, the following text is printed:
** MSC <MSC name> NOT VERIFIED **
|
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 Using High-Level MSCs. (It also means that you may have to reset the validator to be able to reach the system start state again.) |
Before an MSC is loaded into the Validator for verification, it is possible to perform instance conversion of the MSC. Instance conversion will convert the name of an instance to another name.
This is useful if you want to verify some, but not all, instances in an MSC with an SDL system. For instance, you may have an MSC describing a complete system but an SDL system for only a part of the system. In this case, you can convert the not wanted instances to be considered as environment in the Validator, without changing the MSC.
Note that if you have more than one instance representing the environment, the environment instances must be separated using channel names.
Instance conversion is performed before an MSC is loaded into the Validator by entering the command " Define-Instance-Conversion FromString ToString" for each instance name to be converted. All instance conversions can be listed by entering the command List-Instance-Conversion, and all instance conversion can be cleared by entering the command Clear-Instance-Conversion.
Consider an MSC with three process instances A, B and C. The SDL system specifies the behavior for instance A, but not for B or C. Before verifying the MSC, B can be converted to "env channelB" and C to "env channelC", where channelB is the existing SDL channel that will be used for communication between the existing A process and the non-existing process B, and channelC is the existing SDL channel that will be used for communication between the existing A process and the non-existing process C.
This is accomplished by entering the Validator commands:
Define-Instance-Conversion B "env channelB" Define-Instance-Conversion C "env channelC"
The MSC can now be verified.
The high-level MSC that are available in MSC'96 provide a very convenient possibility to describe how many small MSCs are combined to form a larger use case or scenario. The Validator support verification of high-level 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 "connected" state from where two features are accessible. These features are described by the MSCs "datatrans" and "finish". If this would be a communication protocol, the "init" might be a connection establishment, and "datatrans" and "finish" successful data transfer and connection release. This situation could be described using the high-level MSC in Figure 473.
|
|
To check this combination of MSCs simply verify the "inres1" high-level MSC and the validator will generate one MSC verification report for each sequence of "leaf MSCs" that can be verified. In this case there will be reports for "init, finish", "init, datatrans, finish", "init, datatrans, datatrans, finish", etc. until the max depth for MSC verification has been reached.
When an MSC verification has been done, the current state of the validator is different depending on how many MSC verification reports has been found:
This is in many cases useful when using MSCs to navigate to a specific system state, especially in combination with command scripts as described in the next section. Note that if the MSC that is verified is an "old style" MSC without high-level MSCs or MSC reference expressions then there will always be at most one MSC verification report and this type of MSCs is thus best when using MSCs for navigation.
An efficient test strategy when incrementally developing SDL systems is to use regression testing. A set of MSCs describe the requirements on the SDL system and new MSCs are incrementally added to the set when new features are implemented in the SDL system. Each time a new feature is implemented the resulting system should be tested against all the old MSCs as well as the new ones, to make sure that no new errors have been introduced.
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.
A command script that when loaded will perform MSC verification for some requirements described as MSCs may look like:
log-on msc.log verify-msc inres1.mrm reset verify-msc init2.msc verify-msc inres2.mrm quit
The command Log-On is used to store the output from the verification on the file msc.log.
Note in Example 167 how the MSC init2 was used to set up the start state for the verification of the high-level MSC inres2.
When verifying an MSC, the parameters of the messages in the MSC can sometimes be crucial and need to be verified, and sometimes be unimportant for the behavior in question. To support this, the verification of MSCs in the Validator allows three different levels of matching of message parameters:
If no parameters are given, all possible actual parameters are accepted. If the signal is sent from the environment to the system, the parameter values that are defined using the test value facility are used by the Validator when exploring the state space of the system.
When only some of the parameters are to be given, only the given parameters are checked during the exploration. The notation used to show that a specific parameter should be ignored during the verification is to simply leave out this parameter in the parameter list. For example, if only the second and fifth parameter should be used during the verification the parameter list would be ",2,,,true" in the MSC. Trailing commas can be left out, so if a signal has five parameters and only the first two are to be verified, the parameter list might be "1,2" which would ignore the last three parameters.
When only some of the parameters are given for a signal from the environment, the rest of the parameters are taken from the test value definitions when executing the signal output during state space exploration.
If all parameters are given, they are of course all checked.
The MSCs that can be loaded into the Validator must comply with the following rules:
The purpose of an observer process is to make it possible to check more complex requirements on the SDL system than can be expressed using MSCs. The basic idea is to use SDL processes (called observer processes) to describe the requirements that is to be tested and then include these processes in the SDL system. Typical application areas include feature interaction analysis and safety-critical systems.
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:
A simple observer process is illustrated in Figure 474.
Figure 474 : A simple observer process
|
|
This process will check if the variable Counter in the Initiator process ever becomes equal to 2.
Two characteristics for the observer processes are:
To use observer processes:
/*#INCLUDE `access.pr' */
In some cases the Observer reports are not convenient and they can then be turned off with the Define-Report-Continue (that will cause the exploration to continue past a reported situation) and the Define-Report-Log command (that can be used to turn off the logging a s specific report type, e.g. Observer reports)
The Access abstract data type is an ADT intended to be used together with observer processes to make it possible to access the internal state of other processes from an observer process. The ADT is defined in the file access.pr that resides in the ADT directory together with the rest of the ADTs supplied together with SDT. Unlike the rest of the ADTs the Access ADT is a special purpose ADT that only works with the Validator kernel.
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
*/
ActivePID : integer -> PId;
/* Return the PId of the process that executes.
Returns NULL if no process executes.
Observer processes are not taken into account.
The integer parameter is a dummy parameter
needed since operators must have parameters. */
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;
EnvOutput : CharString -> Boolean;
/* Returns true if the transition currently
executing is caused by a signal from the
environment with a specified name, otherwise
false
par 1: The name of the signal type */
The Access ADT also includes a utility procedure called Report that if called from an observer process will generate an Assertion report in the validator. The procedure takes a charstring as parameter and this is the string that will be presented in the Assertion report.
An example of the usage of some of the operators is:
P := GetPId( `Initiator', 1 ), CS := GetState( P )
This example assigns the PId value of the first Initiator process to the PId variable P, and then assigns the name of the state of this process to the charstring variable CS.
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')
In this example we assume that we have a PId variable P that identifies a process that has a variable Var of type for which a v operator is defined. The statement will access the value of Var and assign it to the local variable LocalVar.
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.
Consider the following structure definition:
newtype MSDUType
struct
id IPDUType;
num Sequencenumber;
data ISDUType;
endnewtype MSDUType;
A v operator for this type can be defined as:
newtype MSDUTypeAccess
literals NotUsedMSDUTypeAccess;
operators
v /*#NAME `XVNAME(MSDUType)'*/ :
PId, charstring -> MSDUType;
/*#ADT (H)
#TYPE
#define MSDUType #SDL(MSDUType)
*/
endnewtype MSDUTypeAccess;
Once this definition is in place, variable values for the complex data type can conveniently be accessed using the new v operator. Note also that it is possible to access the values of the fields of the structure in a simple way:
LocalVar := v(P,'MSDUVar')!id
However, if the values of the complex type only is accessed in a few places, it is possible to access them directly using the #CODE operator as illustrated in the following example:
LocalVar := #CODE(`XVV(#SDL(P),"Var",#SDL(MyType))')
In this example we assume that we have a PId variable P that identifies a process that has a variable Var of type MyType. The statement will access the value of Var and assign it to the local variable LocalVar.
A problem common to all state space exploration techniques is related to the treatment of the environment of the SDL system under analysis. As an example, consider the situation during state space exploration where a signal with an integer parameter can be received from the environment. Since there is an infinite number of integer values, there will be an infinite number of successors of the current system state: one where the parameter value is 0, one where the parameter value is 1, etc.
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:
The second strategy is the most common and the test value feature of the Validator is designed to make it easy to define the signals from the environment.
When the Validator is started a list of signals is automatically computed that will be used as the possible signals from the environment during state space exploration. The signal list is generated based on the concept of test values. Test values can be defined for data types and for signal parameters. When generating the signal list the Validator checks for each signal that can come from the environment which test values are defined for its parameters (or for the parameter data types). It then generates one signal instance for each combination of test values for the parameters.
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 simple 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 |
Bit |
0, 1 |
Octet |
00, FF |
For other data types, test values are determined according to the following:
Two restrictions are posed on the computed test values:
Two commands exist for setting options related to the above restrictions:
|
Note: These options affect the state space; see Affecting the State Space. |
The default test values are defined to be useful for a large number of applications, but they sometimes need to be modified. In some cases there are unnecessarily many test values and to enhance the performance of the state space exploration some test values can be cleared. In other cases the automatic test value generation cannot handle some of the data types used, so the test values must be manually defined.
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. |
Test values can be defined and cleared on three "levels": on data types, on individual signal parameters, and on signal instances. When test values are defined or cleared, the list of signals from the environment is regenerated. You are recommended to define test values either on data types and individual signal parameters, or on signal instances; do not combine both these methods.
The monitor commands concerning test values are available in the Test Values module in the Validator UI.
The following commands operate on the test values for a data type (sort).
Define-Test-Value integer 20
The following commands operate on the test values for individual parameters to a signal.
Define-Parameter-Test-Value Score 1 -5
The following commands operate on the test values for a specific signal instance.
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. |
.mpr) and extracts all signals sent from the environment axes to the system axis. If a signal definition is found which does not already exist, it is added automatically by calling Define-Signal.The current set of test values can be saved on file and later be recreated by reading in the file again. The file will contain monitor commands that recreates the saved set of test values and discards any other 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.
The Ref generator (see The Ref Generator) is used to create pointer structures to be used in SDL systems. The Validator supports the Ref generator, but imposes some restrictions on the usage of it due to the special requirements caused by state space exploration.
Variables that are defined to be Ref's to something can be used in two ways, either as a pointer to some other variable or as a pointer to a dynamically allocated memory area. Both ways of using Ref types are supported by the Validator.
To handle dynamically allocated data areas the Validator creates a special data structure as part of each system state. This data structure is a list of all data areas allocated by Alloc (the Ref operator that allocates a new data area) and data areas allocated in external C code (see Validating Systems with External C Code). The list contains for each data area in addition to the area itself information about e.g. the sort of the data area and the size of the data area. Whenever the Validator copies a system state, the list of dynamically allocated data areas is also copied and all Ref variables are set up corresponding to the new copy of the list.
Some restrictions/simplifications are needed when using Ref sorts in the Validator:
Note that the handling of pointers in the Validator introduces a significant overhead that unfortunately reduces the number of transitions per second that is executed by the Validator.
When performing state space exploration, the Validator checks the usage of Ref variables when copying system states and reports several different types of problems including:
For more information about the reports see REF Errors.
SDT allows the usage of external C code together with an SDL system and this is also true for the Validator. In many cases it is possible to directly use the Validator on a system that uses external C code. However, due to the special requirements of state space exploration, some restrictions must hold for the external C code, and some modifications may have to be done to the external code to make it functions properly with the Validator.
To be able to perform a state space exploration it must be possible for the Validator to make a complete copy of a system state, including all data structures that are implemented directly in C code. The Validator must also be able to modify each copy of a system state separately. This has some implications:
If there are variables in C code, this will not be detected by the validator. It may appear as if the Validator works, but the variables defined in C code will not be copied when the Validator copies a system state. When the value of a variable is changed by an action performed in one system state, this value will change the value for all system states that the Validator currently handles. This implies e.g. that when the Validator backtracks during an automatic exploration to test more possible successors of a particular system state, the values of variables defined in C may be different from the values they had the previous time the system state was visited and the state space exploration will not be correct.
In order to be able to copy a system state, the Validator must have exact information about the sort of all data areas in the system to be able to copy e.g. pointer-based data structures correctly. One consequence of this is that the Validator cannot support the C union sort if the union may contain pointer-based sorts, since the Validator cannot know the current sort of the union and thus cannot deduce whether to treat the union as a pointer or not. SDL PIds are also treated specially in the Validator and can also not be part of a C union.
Pointers are frequently used in C code and when used together with SDT they are treated as the (nonstandard) SDL type Ref. The Validator handles the Ref types in a particular way (see Validating Systems That Use the Ref Generator) and the restrictions on variables of this sort also applies to the usage of C pointers in data type in external C code.
When using dynamic memory allocation in extern C code some special additions are needed for the Validator to work properly. This is needed since the Validator keeps a list of all dynamically allocated data areas as part of each system state. If an external C function allocates memory, the Validator must be informed about the data area that was allocated, and the same holds when a C function releases memory. This is accomplished by calling two functions from the C code:
extern void UserMalloc (void *data); extern void UserFree (void *data);
UserMalloc should be called when a data area has been allocated, and UserFree should be called immediately before the data area is released. Both functions should have a pointer to the data area as parameter.
The purpose of UserMalloc is to insert a new element into the list of dynamically allocated data areas that is maintained by the Validator. Note that there is no need to tell the Validator what sort of data was allocated or its size. This is handled automatically by the Validator simply by finding the SDL entity (e.g. a variable) that points at the data area and assuming that the sort and size given by this entity is correct. If no SDL entity can be found that points to the data area, this is considered to be an error and a Validator report is generated.
The purpose of the UserFree function is to inform the Validator that a data area has been released, and thus should be removed from the list of dynamically allocated data areas.
There exists a special C macro XVALIDATOR_LIB that can be used to check in external C files if the code is compiled together with the Validator kernel. It is thus possible to only include the calls to UserMalloc/UserFree when the C code is compiled together with the Validator using this macro, as in the following example:
... v = malloc( 10 ); #ifdef XVALIDATOR_LIB UserMalloc( (void *)v ); #endif
In the Validator, you may define a user-defined rule to be used during state space exploration to check for properties of the encountered system states. If a system state is found for which the user-defined rule is true, a report will be generated. Note that only one user-defined rule may be defined at a time.
There are three different situations in which a user-defined rule is useful:
An example of a rule that checks a system property is:
exists P:Proc | P->var=12;
which is true for all system states where there exists a process of type "Proc" with a variable "var" that is equal to 12.
A simple example of a rule that searches for a system state is:
state(initiator:1)=disconnected;
which is true for all system states where the process instance
"initiator:1" is in the state "disconnected".
A more complex example of such a rule is:
state(Game:1)=Winning and sitype(signal(Game:1))=Probe
which is true for all system states where the state of the process instance "Game:1" is equal to "Winning" and the type of signal to be consumed by the same process instance is "Probe".
An example of a rule that reduces the state space is:
(Game:1->Count > 2) or (Game:1->Count < -2)
which is true for all system states where the absolute value of the variable "Count" in the process instance "Game:1" is greater than 2.
For a full description of the features and syntax of user-defined rules, see User-Defined Rules.
To define the user-defined rule, select Define Rule from the Commands menu, or enter the command Define-Rule, followed by the definition of the rule.
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.
Like most other run-time libraries to the C Code Generator, the Validator library gives the user a possibility to define his own run-time errors or assertions. An assertion is a test that is performed at run-time, for example to check that the value of a specific variable is within the expected range. Assertions are described by introducing #CODE directives with calls to the C function xAssertError in a TASK. See the following example.
TASK '' /*#CODE
#ifdef XASSERT
if (#(I) < #(K))
xAssertError("I is less than K");
#endif
*/ ;
In the SDT Validator, the assertions are checked during state space exploration. Whenever xAssertError is called during the execution of a transition, a report is generated. The advantage of using this way to define assertions, as opposed to using user-defined rules, is that in-line assertions are computed much more efficiently by the validator than the user-defined rules.
The xAssertError function, which has the following prototype:
extern void xAssertError ( char *Descr )
takes a string describing the assertion as parameter and will produce an SDL run-time error similar to the normal run-time errors. The function is only available if the compilation switch XASSERT is defined. For the standard libraries this is true for all libraries except the Application Library.
This section describe the various possibilities available to control the behavior of the Validator 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.
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 Validator 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 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 (on UNIX), or valinit.com (in Windows), 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:
|
Note: This command also resets the validator completely and is equivalent to restarting the validator from scratch. To just set the options to their initial values without resetting the validator:
|
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 validator 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 475 : 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 is an efficient automatic state space exploration algorithm for reasonably large SDL systems (for a reference, see [15]). 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:
The search depth is the maximum depth the Validator 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.
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 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.
The search depth determines how many transitions will be executed before the search is pruned and restarted from the beginning again.
The number of times the random walk search will be repeated from the start state before the exploration is finished.
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.
The search depth is the maximum depth the Validator 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.
The MSC verification algorithm is a bit state exploration that is adapted to suit the needs of MSC verification:
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.
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.
For each report type, you can define the action performed when the report is found and whether it should be reported to the user.
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.
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.
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.
When the Validator performs an MSC trace, you can define what types of events that are traced.
By default, actions like tasks, decisions, etc. are not shown in the MSC trace. You may change this by setting action trace to On.
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.
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.
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 Validator immediately useful for as many applications as possible. This, however, also means that the search performed by the Validator 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.
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.
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 SDT Code Generator 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.
The events that are represented in a behavior tree can be divided into five classes:
none.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.
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 validator 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.
The Validator 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).
The length of the input port queues is not infinite in the Validator, 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.
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.
To avoid infinite chains of create actions in the state space, the Validator 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.
When the Validator 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 Validator can handle.
One test that can be made with the Validator 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.
One test that can be made with the Validator 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.
See section Computing Test Cases for a discussion of the Autolink 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:
[15]
Holzmann, G.J:
Design and Validation of Computer Protocols
Prentice-Hall, 1991
ISBN 0-13-539834-7