IBM
Contents Index Previous Next



Verifying a Message Sequence Chart


Another main area of use for an SDL Explorer 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 name of the MSC file is SystemLevel.msc and is located in the same directory as the remaining files for the DemonGame example. The MSC is shown in the figure below.

Figure 143 : A system level MSC

  1. 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 Explorer and start it again.
  2. Start an MSC verification by clicking the Verify MSC button. A file selection dialog is opened, in which you select the MSC to verify.
  3. Select SystemLevel.msc and click OK. A state space exploration is now started, which is guided by the loaded MSC.
    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 144 : Violations and verifications of the MSC

  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:
    *   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 143. 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 explorer is always made on the process level.

Figure 145 : The MSC trace

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

Exiting the SDL Explorer UI

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

  1. 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 Explorer UI from the File menu. You may be asked in a dialog whether to save changes to the Explorer options.

Figure 146 : Saving changed options

  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 Explorer UI is started from the same directory, or when the explorer is restarted or reset from the Explorer UI. You should select No and click OK.

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