[Previous] [Next] [Contents] [Index]

    Tutorial: The SDT Validator

The SDT Validator is the tool that you use for validating the behavior of your SDL systems, using state space exploration techniques. In this chapter, you will practice "hands-on" on the DemonGame system.

To be properly assimilated, this tutorial therefore assumes that you have gone through the exercises that are available in Tutorial: The Editors and the Analyzer as well as Tutorial: The SDT Simulator.

In order to learn how to use the Validator, read through this entire chapter. As you read, you should perform the exercises on your computer system as they are described.

Table of Contents 

Purpose of This Tutorial

The purpose of this tutorial is to make you familiar with the essential validation functionality in SDT. With validation we mean exploring the state space of an SDL system with powerful methods and tools that will find virtually any kind of possible run-time errors that may be difficult to find with regular simulation and debugging techniques.

This tutorial is designed as a guided tour through SDT, where a number of hands-on exercises should be performed on your computer as you read this chapter.

We have on purpose selected a simple example that should be easy to understand. It is assumed that you have a basic knowledge about SDL -- this chapter is not a tutorial on SDL.

It is assumed that you have performed the exercises in Tutorial: The Editors and the Analyzer as well as Tutorial: The SDT Simulator before starting with the tutorial on the Validator.

Note:  C compiler

You must have a C compiler installed on your computer system in order to validate an SDL system. Make sure you know what C compiler(s) you have access to before starting this tutorial.

Note:  Platform differences

This tutorial, and all tutorials that are possible to run on both the UNIX and Windows platform, are described in a way common to both platforms. In case there are differences between the platforms, this is indicated by texts like "on UNIX", "Windows only", etc. When such platform indicators are found, please pay attention only to the instructions for the platform you are running on.

Normally, screen shots will only be shown for one of the platforms, provided they contain the same information for both platforms. This means that the layout and appearance of screen shots may differ slightly from what you see when running SDT on your computer screen. Only if a screen shot differs in an important aspect between the platforms will two separate screen shots be shown.

Generating and Starting a Validator

In addition to simulating a system, it is also possible to validate the system using the SDT Validator. A validator can be used to automatically find errors and inconsistencies in a system, or to verify the system against requirements.

In the same way as for a simulator, you must generate an executable validator and start it with a suitable user interface.

Note: 

In order to generate a validator that behaves as stated in the exercises, you should use the SDL diagrams that are included in the Telelogic Tau distribution instead of your own diagrams. To do this:

  • On UNIX: Copy all files from the directory
    $telelogic/sdt/examples/demongame
    to your work directory ~/demongame.
  • In Windows: Copy all files from the directory
    C:\tau35\sdt\examples\demongame
    to your work directory C:\tau35\work\demongame.

If you generate a validator from the diagrams that you have created yourself, the scheduling of processes (i.e. the execution order) may differ.

If you choose to copy the distribution diagrams, you must then re-open the system file demongame.sdt from the Organizer.

What You Will Learn

Quick Start of a Validator

A validator can be generated and started in the same way as described earlier for the simulator, i.e., by using the Make dialog and the Tools menu in the Organizer. However, we will now show a quicker way.

  1. Make sure the system diagram icon is selected in the Organizer.

  2. Extracted pic [26] Click the Validate quick button. The following things will now happen, in rapid succession:

Note: 

If you receive errors from the Make process (in the Organizer Log window) or if no Validator is started, do as follows:

  • Open the Make dialog and change to a Validation kernel reflecting the C compiler used on your computer system, e.g.
    gcc-Validation or Microsoft Validation.
  • Click the Full Make button and check that no errors where reported.
  • Click the Validate quick button again. A Validator should now be started as described above.

The Validator UI looks like this:

Figure 136 : The main window of the Validator UI

Extracted pic [19]

As you can see, the graphical user interface of a validator is very similar to a simulator GUI, which you have learned to use in the previous exercises. However, the button modules to the left are different and a few extra menus are available.

A validator contains the same type of monitor system as a simulator. The only difference is the set of available commands.

When a validator is started, the static process instances in the system are created (in this case Main and Demon), but their initial transitions are not executed. The process in turn to be executed is the Main process. You can check this by viewing the process ready queue:

  1. Locate the button module View in the left part of the window, and click the Ready Q button. The first entry in the ready queue is Main, waiting to execute its start transition.

Figure 137 : A collapsed button module

Extracted pic [20]

  1. If required, resize the Validator UI window so that all button modules are visible. You may also reduce the width of the text area. In the exercises to come, you will have a number of windows open at the same time.

Basics of a Validator

Before you start working with the validator exercises, you should have an understanding about the basic concepts of the SDT Validator.

Navigating in a Behavior Tree

In this first exercise, we will explore the state space of the Demongame system by manually navigating in the behavior tree. The validator will then behave in a way similar to when running a simulator. However, there are also important differences, which will be pointed out.

By default, the validator is set up in a way that results in a state space as small as possible. In this set-up, a transition between two states in the behavior tree always corresponds to a complete transition in the SDL process graphs. Also, the number of possible branches from a state is limited to a minimum.

What You Will Learn

Setting Up the Exploration

When interactively exploring the behavior tree, a validator tool called the Navigator is used.

  1. Start the Navigator by clicking the Navigator button in the Explore module. The Navigator window is opened:

Figure 138 : The Navigator tool

Extracted pic [21]

  1. To be able to see the printed trace familiar from simulation, open the Command window from the View menu. (The trace is not printed in the main window of the validator.)
  2. To switch on GR trace of SDL symbols, select Toggle SDL Trace from the Commands menu in the Validator window; SDL trace is now enabled. However, an SDL Editor will not be opened until the first transition is executed.

Using the Navigator

  1. In the Navigator, execute the next transition by double-clicking on the Next 1 node. The following happens, in order:

Figure 139 : The last and next transition

Extracted pic [1]

Figure 140 : The printed trace for the executed transition

Extracted pic [22]

  1. If needed, move and resize all opened windows to make them completely visible and still fit on the screen together.
  2. Double-click the Next 1 node to execute the next transition. The start transition of Demon is traced in the Command window and in the SDL Editor.

    3. At this stage, neither of the two active processes can continue without signal input: Main awaits the signal Newgame from the environment, and Demon awaits the sending of the timer signal T. These are the two transitions from the current state now shown in the Navigator as Next 1 and Next 2. As you can see, the transitions in the boxes are described by the same type of information as in a printed trace.

Figure 141 : Transition descriptions in the Navigator

Extracted pic [2]

  1. Send the timer signal by double-clicking the Next 2 node. The Command window tells us that the timer signal is sent and the Navigator shows that the next transition is the input of the timer T.
  2. Execute the next transition by double-clicking the Next 1 node. This is where the dynamic error in the Demongame system occurs, as explained in the simulator tutorial earlier (see Dynamic Errors). Instead of showing the next transition, the Navigator displays the error message in the next box.

Figure 142 : The dynamic error

Extracted pic [3]

Figure 143 : The tail of the Print-Trace module

Extracted pic [23]

  1. Double-click the Up 1 node to go back to the previous state. Repeat this action again to go to the state we were in after step 3 above. This way of backing up in the execution is not possible when running a simulator, as you may have noticed when running the Simulator tutorial.

    2. You should also note that the Next 2 node is marked with three asterisks "***." This is used to indicate that this is the transition we have been backing up through:

Figure 144  : Marking a transition that has been backed through

Extracted pic [4]

  1. Execute the Next 1 transition instead. The printed trace shows that the signal Newgame was sent from the environment. The Main process is ready to receive the signal. Note that you do not have to send the signal yourself; this is taken care of automatically by the validator.
  2. Execute the next transition. The printed trace and the SDL trace show that Main now is in the state Game_On. The Navigator displays the start transition of the newly created Game process.
  3. Execute the start transition of Game. The Navigator will now show the different signal inputs that are required to continue execution: Endgame, Probe, Result, and the timer T.

Figure 145 : Signal inputs required for continued execution

Extracted pic [5]


  1. Extracted pic [27] Click the Toggle Tree quick-button to see how the list structure looks like. Now it is easier to see the possible signals.

Figure 146 : The list structure

Extracted pic [6]

  1. Change back to the tree structure.

    2. We will not continue further down in the behavior tree in this exercise. Figure 147 shows the part of the behavior tree we have explored so far. The nodes in the figure represent states of the complete SDL system. Each node lists the active process instances that have changed since the previous system state, what process state they are in and the content of their input queues. The arrows between the nodes represent the possible tree transitions. They are tagged with a number and the SDL action that causes the transition. The arrow numbers are the same numbers as printed in the Next nodes in the Navigator.

    Note that this is a somewhat different view of the behavior tree compared to the Navigator. In the Navigator, the nodes represent the tree transitions and the process states are not shown.

Figure 147  : A Demongame behavior tree

Extracted pic [7]

More Tracing and Viewing Possibilities

In this exercise, we will take a look at some of the additional tracing and viewing possibilities of the validator.

What You Will Learn

Using the View Commands

  1. Make sure you are still in the same state as after the last step in the previous exercise.

    2. To see a complete printed trace from the start state to the current state, you can use the Print-Trace command. As parameter, it takes the number of levels back to print the trace from.
  2. On the input line of the Validator UI, enter the command pr-tr 9 (you can use any large number). The trace is printed in the text area of the main window. This trace gives an overview of what has happened in the SDL system so far.
  3. The Validator supports the same viewing possibilities as the SDT Simulator. Click the Timer List button in the View module to list the active timer set by the Demon process.
  4. Examine the GameP variable in the Main process by first setting the scope to the Main process (click the Set Scope button and select the Main process), and then clicking the Variable button and selecting the GameP variable.

Using MSC Trace

In addition to textual and graphical traces, the validator can also perform an MSC trace.

  1. First, turn off SDL trace by selecting Toggle SDL Trace from the Commands menu. Then, turn on MSC trace from the same menu. An MSC Editor is opened, showing a Message Sequence Chart for the trace from the start state to the current state.

Figure 148 : The current MSC trace

Extracted pic [8]

  1. When the MSC appears, execute, with a double-click, one of the signal transitions in the Navigator, e.g. Probe. The message is appended to the MSC (but it is not yet consumed).
  2. Go up a few levels in the Navigator.

    3. Note how the selection in the MSC Editor changes to reflect the MSC event corresponding to the current state!
  3. Go down again, but select a different path than before, i.e., send one of the other signals.

    4. Note how the MSC diagram is redrawn to show the new behavior of the system!
  4. Toggle MSC trace off in the Commands menu. Unless other MSC diagrams were opened, the MSC Editor is closed.

Going to a State Using Path Commands

You can use the commands Print-Path and Goto-Path to return to a state where you have been before.

  1. Execute the command Print-Path from the input line. The output represents the path taken in the behavior tree from the start state to the current state. 

    2. Command : print-path
1 1 1 1 1 3 0
  2. Go up a few levels in the Navigator.
  3. In the text area, locate the path printed by the Print-Path command above (you may have to scroll the text area). On UNIX, select the numbers in the path with the mouse by dragging the mouse to the end of the line. Make sure you select the final zero.
  4. In the input line, enter goto-path and the path printed by the Print-Path command. On UNIX, paste in the path numbers by positioning the mouse pointer at the end of the entered text and clicking the middle mouse button.
  5. Hit <Return> to execute the command. You now end up in the previous state.

Validating an SDL System

In the previous exercises, we have navigated manually in the behavior tree. We have also found an error situation by studying the Navigator and the printed trace in the Command window.

In this exercise, we will show how to find errors and possible problems by automatically exploring the state space of the Demongame system. This is referred to as validating an SDL system.

What You Will Learn

Performing a Bit State Exploration

Automatic state space exploration can be performed using different algorithms. The algorithm called bit state exploration can be used to efficiently validate reasonably large SDL systems. It uses a data structure called a hash table to represent the system states that are generated during the exploration.

An automatic state space exploration always starts from the current system state. Since we want to explore the complete Demongame system, we must first go back to the start state of the behavior tree.

  1. Go to the top of the tree by clicking the Top button in the Explore module.
  2. Start a bit state exploration by clicking the Bit-State button. After a few seconds, a tool called the Report Viewer is opened. We will soon describe this window; in the meantime, just move it away from the main window.
  3. For a small system such as Demongame, the exploration is finished almost immediately and some statistics are printed in the text area. They should look something like:

    4. ** Starting bit state exploration **
Search depth    : 100
Hash table size : 1000000 bytes

** Bit state exploration statistics **
No of reports: 1.
Generated states: 2569.
Truncated paths: 156.
Unique system states: 1887.
Size of hash table: 8000000 (1000000 bytes)
No of bits set in hash table: 3642
Collision risk: 0 %
Max depth: 100
Current depth: -1
Min state size: 68
Max state size: 124
Symbol coverage : 100.00
    Of the printed information, you should note the following:

Examining Reports

The error situations reported from a state space exploration can be examined in the Report Viewer. The Report Viewer window displays the reports in the form of boxes in a tree structure.

Figure 149 : The Report Viewer

Extracted pic [24]

  1. To expand the report, double-click on the report type box Output. You will now see a box reporting the error we have found manually earlier. In addition, the tree depth of the error situation is shown.

Figure 150 : An expanded report

Extracted pic [9]

  1. Double-click the report box in the Report Viewer. The following things will now happen:
    2. Once you have used the Report Viewer to go to a reported situation, you can easily move up and down the path to this state. Simply use the Up and Down buttons in the Explore module, instead of double-clicking a node in the Navigator:
  2. Move up two steps by using the Up button. Of the two transitions possible from this state, the one that is part of the path leading to the error is indicated by three asterisks "***" (see Figure 144). This is the transition chosen when using the Down button.
  3. Move up to the top of the tree (click the Top button in the Explore module). Move down again to the error by using the Down button repeatedly.

    4. Note that you do not have to chose which way to go when the tree branches. The path to the error is remembered by the validator until you manually chose another transition.

Exploring a Larger State Space

We will now run a more advanced bit state exploration, with a different setting of the state space options. This will make the state space much larger, so that more error situations can be found.

  1. Go back to the top of the behavior tree (use the Top button).
  2. In the Options1 menu, select Advanced. This sets a number of the available state space options in one step, as you can see by the commands executed in the text area:

    3. Command : def-sched all

Command : def-prio 1 1 1 1 1

Command : def-max-input-port 2
Max input port length is set to 2.

Command : def-rep-log maxq off
No log for MaxQueueLength reports
    Note that the Navigator now shows two possible transitions from the start state; this is an immediate effect of the larger state space.
  3. In addition, we will increase the search depth of the exploration from 100 (the default) to 300. From the Options2 menu, select Bit-State: Depth. In the dialog, enter 300 and click OK.

Figure 151 : Specifying Depth = 300

Extracted pic [15]

  1. Start a new bit state exploration. In the text area, a status message is printed every 20,000 transitions that are executed. Stop the exploration after one of the first status messages by pushing the Break button in the Explore module. The text area should now display something like this:

    2. *** Break at user input ***

** Bit state exploration statistics **
No of reports: 2.
Generated states: 50000.
Truncated paths: 1250.
Unique system states: 21435.
Size of hash table: 8000000 (1000000 bytes)
No of bits set in hash table: 41557
Collision risk: 0 %
Max depth: 300
Current depth: 235
Min state size: 68
Max state size: 168
Symbol coverage : 100.00

Note: 

If the exploration finishes by itself before you have had a chance to stop it manually, redo this exercise from step 1. but increase the search depth even more, e.g. 400 or 500.

  1. In the Report Viewer, open the two report type boxes to see both reports with a double-click on each. The Report Viewer window should now look something like:

Figure 152 : The two reports as displayed in the window

Extracted pic [25]

  1. For now, just note on which depth each of the reported situations occurred; do not double-click any of the reports. (The depths may be different from the ones shown in the figure.)
  2. Continue the exploration by clicking the Bit-State button again. A dialog is opened, asking if you would like to continue the interrupted exploration or restart it from the beginning.

Figure 153 : Continuing the exploration

Extracted pic [16]

  1. In the dialog, select Continue and click OK. Wait for the exploration to finish by itself.
  2. In the Report Viewer, open the two reports again. Note that the depth values have changed. This is because only one occurrence of each report is printed; the one found at the lowest depth so far.
  3. Go to the state where an unsuccessful create of the Game process was reported (double-click the Create report).

Figure 154 : The report about an unsuccessful process create

Extracted pic [10]

  1. To see what caused the unsuccessful create, look at the MSC trace.

    2. At the receipt of the last Newgame signal, the Main process attempts to create a Game process. However, the already active Game process has not yet consumed the previous GameOver signal, and has therefore not been terminated. Since you cannot have more than one instance of the Game process in the Demongame system, the process create could not be executed!

Restricting the State Space

The Validator makes it possible to limit the state space in several different ways. We will now explore one of these methods that in many cases is very efficient. This is done by using the Define-Variable-Mode command.

This command is used to instruct the Validator to ignore certain variables when matching states during the state space exploration. The mode can for each variable be set to either "Skip" or "Compare". The implication of setting the mode to "Skip" is that the search may be pruned even if a new state is encountered during the search. This happens if the only difference between the new state and a previously visited state is that the values of some of the skipped variables are different.

We will now apply this to our DemonGame system. The variable Count in the Game process keeps track of the current score for the game, and the value of this variable does not have any real impact on the behavior of the system. So, we will now instruct the validator to ignore this variable when performing a search.

  1. Go to the top of the tree by clicking on the Top button.
  2. Enter the command define-variable-mode in the command line in the Validator UI, select the Game process in the first dialog, the Count variable in the second dialog and Skip in the last dialog. You have now instructed the Validator to ignore the Count variable.
  3. Start a bit state exploration by clicking on the Bit-State button. (Select to Restart the exploration if a dialog is opened.)
  4. When the search stops compare it with the previous exploration. The only difference between the two explorations is that the second one ignores the Count variable. However, while the first exploration took a long time to finish, the second one only took a few seconds! The printed statistics show very small numbers in comparison.

The lesson to learn from this is that it in many cases it is possible to drastically reduce the time needed for explorations by checking the variables in the system. Look for variables that do not have any impact on the behavior (i.e. that does not influence decision statements or the expression used in an "output to" statement). Also look for variables that do not change their value during the exploration. This can for example be arrays that are initialized at system start up but then never changes (or at least not changed in the intended exploration). The mode for these types of variables should be set to "Skip".

Checking the Validation Coverage

If the symbol coverage after an automatic state space exploration is less than 100%, the Coverage Viewer can be used to check what parts of the system that have not been executed. To attain a symbol coverage less than 100% for the Demongame system, we will set up the exploration in a special way.

  1. Go to the top of the tree.
  2. First, we need to restore the smaller, default state space. Select Default from the Options1 menu. Note that the Navigator changes back to display only a single possible transition from the top node.
  3. To avoid reaching all system states, we will reduce the search depth of the exploration from 100 to just 10. Use the Bit-State: Depth menu choice from the Options2 menu and specify a maximum depth of 10.
  4. Start a bit state exploration. The printed statistics should now inform you that the symbol coverage is about 82%.
  5. To find out which parts of the Demongame system that have not been reached, open the Coverage Viewer from the Commands menu.

    6. A symbol coverage tree is displayed, showing all symbols which have not been executed yet.

  6. Extracted pic [28] Change to a transition coverage tree by clicking the Tree Mode quick-button.

Figure 155 : The transition coverage tree

Extracted pic [11]

Going to a State Using User-Defined Rules

To go to a particular system state, you could use the Navigator to manually find the state by studying the transition descriptions and the printed trace in the Command window. This can be both tedious and difficult, especially for larger systems than Demongame. Instead, we will show an easier way: by using a user-defined rule.

When performing state space exploration, the validator checks a number of predefined rules in each system state that is reached. It is when such a rule is satisfied that a report is generated.

In this exercise, we will show how to define a new rule to be checked during state space exploration. The rule will be used to find the state Winning in the Game process.

  1. Make sure you still are at the top of the behavior tree.
  2. Define a new rule by selecting Define Rule from the Commands menu. In the dialog that appears, enter the rule definition
    state(Game:1)=Winning

Figure 156 : Specifying a new rule

Extracted pic [17]

  1. Start a bit state exploration. Since we have not changed any of the options since the last exploration the same statistics will be printed, with the exception that an additional report is generated.
  2. From the Report Viewer, go to the reported situation where the user-defined rule was satisfied. You have now reached the first place in the behavior tree where the Game process is in the state Winning.
  3. We now instruct the validator to use this state as the root of the behavior tree. To do this, enter the command define-root on the input line and select Current in the dialog.

We can now change options, define a new rule or load an MSC. These new settings will then be used in all explorations based on the new root. Also all list/goto-path commands will use the path from the new root and the MSC trace will give the trace from the new root.

  1. Before continuing, do not forget to clear the user-defined rule. To do this, enter the command clear-rule on the input line.

In our case we will only clear the rule and start another type of state space exploration from this state; a random walk.

Performing a Random Walk

Apart from bit state exploration, there is another exploration method known as random walk. A random walk simply explores the behavior tree by repeatedly choosing a random path down the tree. This is mainly useful for SDL systems where the state space can be very large. But also for a small system like Demongame, it can be as effective as other exploration methods.

  1. Start a random walk exploration from the current state by clicking the Random Walk button. From the printed statistics, you can see that the symbol coverage now has become 100%.
  2. Load the Coverage Viewer with the new coverage information by selecting Show Coverage Viewer from the Commands menu. Change to transition coverage and display the whole tree. Note that all transitions have executed a large number of times. When the exploration selects a random path down the tree, there is no mechanism to avoid that already explored paths are explored once more. Therefore, the same transition may be executed any number of times
  3. Exit the Coverage Viewer from the File menu.
  4. Reset the system by selecting Reset from the Options1 menu. You are now back at the top of the tree, and the root of the tree is reset to the original root, the start state of the system.

Verifying a Message Sequence Chart

Another main area of use for a validator is to verify a Message Sequence Chart. To verify an MSC is to check if there is a possible execution path for the SDL system that satisfies the MSC. This is done by loading the MSC and performing a state space exploration set up in a way suitable for verifying MSCs.

What You Will Learn

Verifying a System Level MSC

In this exercise, we will verify one MSC made on the system level, i.e., an MSC that only defines signals to and from the environment. The MSC is included in the SDT distribution and is shown in the figure below. The name of the MSC file is SystemLevel.msc and is located in the same directory as the remaining files for the DemonGame example.

Figure 157  : A system level MSC

Extracted pic [12]

  1. From the operating system, make sure you can locate the MSC mentioned above (SystemLevel.msc). Make a copy of the MSC and put it in your tutorial directory.
  2. Reset the system. This time do it by choosing Restart in the File menu. Choose "No" if you are asked to save options. The Restart command will actually terminate the running Validator and start it again.
  3. Start an MSC verification by clicking the Verify MSC button. A file selection dialog is opened, in which you select the MSC to verify.
  4. Select SystemLevel.msc and click OK. A state space exploration is now started, which is guided by the loaded MSC.

    5. In the printed statistics, note that the exploration is completed without any truncated paths. This is because the loaded MSC restricts the size of the behavior tree; only the parts dealing with the events in the MSC are executed. The maximum depth of it is not more than 20.

    Note the line that tells if the MSC was verified or violated:

    ** MSC SystemLevel verified **
    In this case the MSC was verified, i.e., the behavior described in the MSC was indeed possible. In the Report Viewer, however, one (or two) of the reports is a violation of the loaded MSC, while the other one is a verification of the MSC. The exploration may very well find states that violate the MSC; it is the existence of states that verify the MSC that determines the result of the verification.

Figure 158 : Violations and verifications of the MSC

Extracted pic [13]

  1. Go to the state where the MSC was verified. The printed trace in the Command window shows that the Main process has received the Endgame signal, and sent the GameOver signal to the Game process:

    2. *   OUTPUT of GameOver. Receiver: Game:1
*     Signal GameOver received by Game:1
  2. Take a look at the MSC trace and compare it with the loaded MSC in Figure 157. Note that the loaded MSC only defines signals to and from the environment and therefore is less detailed than the MSC trace. An MSC trace in the validator is always made on the process level.

Figure 159 : The MSC trace
The trace in the figure does not show the condition symbols that indicates the state of the processes.

Extracted pic [14]

Exiting the Validator UI

The first part of the validator tutorial is now finished. Close the validator windows in the following way:


  1. Extracted pic [29] To close the Navigator and the Report Viewer, click the Close quick button in these windows.
  2. To close the Command window, select Close from the File menu.
  3. Exit the Validator UI from the File menu. You may be asked in a dialog whether to save changes to the Validator options.

Figure 160 : Saving changed options

Extracted pic [18]

  1. If you select Yes and click OK, the option settings are saved in a file called .valinit (on UNIX), or valinit.com (in Windows). This file is read each time the Validator UI is started from the same directory, or when the validator is restarted or reset from the Validator UI. You should select No and click OK.

Using Test Values

In this final exercise we will explore the test value feature in the Validator. This feature is used to control the way the environment interacts with the system during state space exploration. In practise, the test values define what signals will be sent from the environment to the system, including the exact values of their parameters.

In this part of the Validator tutorial we will use another SDL system, theInres system.

  1. Copy the Inres system from the SDT installation to a working directory of your own. Copy all files from the directory $telelogic/sdt/examples/inres (on UNIX), or C:\tau35\sdt\examples\inres (in Windows).

What You Will Learn

Using the Automatic Test Value Generation

When the Validator is started, test values for a number of SDL sorts are automatically generated. For example, all integer parameters will have the test values -55, 0 or 55. We will now take a look at the automatically generated test values for the Inres system.

  1. Open the Inres system file from the Organizer's File menu. If any part of the existing DemonGame system needs saving, you are first prompted to do so before the Open file dialog appears. Locate the file inres.sdt that you have copied and open it.
  2. Generate and start a Validator for the system by clicking on the Validate quick button; see Quick Start of a Validator for more information. If you are asked in a dialog whether to start a new Validator UI or use an existing one, select the existing validator in the list and click OK.
  3. Expand the Test Values button module in the Validator UI and make the window bigger so you can see all the buttons.

    4. The button module contains three rows of buttons. The top three buttons List Value, Def Value And Clear Value make it possible to define test values for each sort (data type) in the SDL system. The middle row with the buttons List Par, Def Par and Clear Par handles test values for specific signal parameters. The bottom row handles test values for entire signals.
  4. Click on the List Value button to see what default test values have been generated. The following values should be listed:

    5. Sort integer:
0
-55
55

Sort Sequencenumber:
zero
one

Sort IPDUType:
CR
CC
DR
DT
AK
    As you can see, there were test values defined for the predefined sort integer and for two system specific enumerated sorts Sequencenumber and IPDUType. For enumerated types, all the values will by default be used as test values if there are 10 or less values. Note that only sorts that appear on parameters to signals to or from the environment are listed.
  5. Click on the List Signal button to see what signals will be sent to the system based on the test values for the sorts.

    6. You should now see a list of signals similar to the following. Note that there might be differences in the parameters to the MDATreq signal since this is computed using a random function that is depending on the compiler used.

    ICONreq
IDATreq(0)
IDATreq(-55)
IDATreq(55)
IDISreq
MDATreq((. CR, zero, -55 .))
MDATreq((. CR, zero, -55 .))
MDATreq((. CC, one, 55 .))
MDATreq((. AK, one, 55 .))
MDATreq((. CR, one, 55 .))
MDATreq((. DT, one, -55 .))
MDATreq((. CC, one, 0 .))
MDATreq((. CC, one, -55 .))

MDATreq((. AK, one, 55 .))
MDATreq((. DR, one, 0 .))
    The signals ICONreq and IDISreq have no parameters so there will only be one signal definition for each of these signals. The IDATreq signal has one integer parameter, and as you can see there will be three test values for this signal, one for each of the test values for the integer sort.

    The MDATreq signal takes a parameter that is a structure with three fields: one IPDUType, one Sequencenumber and one integer. Whenever the Validator finds a structure, it tries to generate test values for the sort based on all combination of test values for each field. However, if the number of test values is larger than a maximum value, a randomly chosen subset is used instead. The maximum number is by default 10, but can be changed with the Define-Max-Test-Values command.

    The consequence of this is that for the MDATreq signal, 10 different randomly chosen parameter values are generated.

    Now, let us check how the test values influence the behavior of the system during state space exploration.
  6. Start the Navigator by clicking on the Navigator button in the Explore button module.
  7. Double-click on the down node 4 times (until there is more than one alternative down node).

    8. You should now have a choice between 11 different down nodes that each one represents an input from the environment to the SDL system. If you check the inputs more carefully, you will see that these 11 inputs correspond to the test values defined for the signals ICONreq and MDATreq.

    This is the way the test values have an impact on the state space exploration. Whenever a signal can be sent from the environment to the system, the Validator uses the test values defined for the signal to determine what parameters to use when sending the signal.

Changing the Test Values Manually

Now, we will use the other commands in the Test Values button module to manually change the test values.

  1. Click on the Top button in the Explore module to return to the start state in the state space.

    2. First we will change the test values for integer to only test the values 1 and 99.
  2. Click on the Clear Value button, select the integer type in the dialog and give the value `-' (a dash) in the value dialog. Dash indicates that we would like to remove all test values currently defined for the sort.

    3. Note that the Validator tries to recompute test values for various sorts and signals when you have changed the test values for integer. Since integer is used in a number of other sorts and signals, the Validator is now unable to compute test values for these sorts and signals.
  3. Check the signal definitions that now is used by clicking on the List Signal button. The current signal definitions should now be:

    4. ICONreq
IDISreq
    Since there are no test values for integer, only the signals that does not contain integer parameters are listed. In this case this means that only ICONreq and IDISreq would have been sent to the system from the environment if you would start an exploration.
  4. Click on the Def Value button, select integer in the sort dialog and give the value 1 in the value dialog.
  5. Click on the Def Value button once more. Select integer in the sort dialog again, but this time give the value 99 in the value dialog.
  6. Click on the List Signal button to check the signal definitions and make sure that the signals with integer parameters are once again on the list. This time with the test values 1 and 99.

    7. ICONreq
IDATreq(1)
IDATreq(99)
IDISreq
MDATreq((. AK, zero, 1 .))
MDATreq((. DR, zero, 99 .))
MDATreq((. AK, one, 1 .))
MDATreq((. DR, one, 1 .))
MDATreq((. DR, zero, 99 .))
MDATreq((. AK, zero, 1 .))
MDATreq((. AK, one, 99 .))
MDATreq((. AK, zero, 99 .))
MDATreq((. AK, one, 1 .))
MDATreq((. CR, one, 1 .))

You have now explored some on the most frequently used test value features in the Validator. There are also possibilities to set test values for specific parameters and to enumerate all signal definitions manually. You can find more information about this in the section Defining Signals from the Environment.

Exiting the Validator

To exit the Validator follow the same steps as before:

  1. Select Exit from the File menu.
  2. Choose Yes when asked whether you want to save the new options or not. To select Yes in this dialog implies that commands that recreates your new test value definitions will be saved in the file .valinit (on UNIX) or valinit.com (in Windows).

So Far ...

By practicing this and the previous tutorials, you have learned the basics of ORCA1 and SDT and we hope you have enjoyed the "tour". The examples you have been practising on, the DemonGame and Inres systems, are however rather simple. To deepen your knowledge about SDT, you may practise on a number of exercises that illustrate the advantages of SDL-92 when adopting an object-oriented design methodology. These exercises are described in Tutorial: Applying SDL-92 to the DemonGame.

1. ORCA is part of the Telelogic product suite and stands for Object oriented Requirement Capture and Analysis.

[Previous] [Next] [Contents] [Index]