Inspect the synthesized SDL model

In the previous exercise we showed how to use the KLOCwork MSC to SDL tool to automatically produce the SDL model from the set of MSCs and HMSCs. In this exercise, we demonstrate how to use the Telelogic Tau SDL Editor to investigate the SDL model.

1. To start the SDL Editor, double-click on the SDL system symbol for SynthesizedModel in the Server module of the Organizer. The SDL Editor displays the diagram of the SynthesizedModel.



A complete set of SDL diagrams for the Server model follows:









The SDL Editor has a palette of graphical symbols (right panel), a graphical editing area and a text editing area (bottom panel). When browsing through the generated SDL model you may want to turn off the graphical symbols palette and the text editing area to make for more room in the main graphical area. To toggle panels on and off, use their corresponding buttons in the quick button panel on top of the graphical editing area.

2. Usually, SDL diagrams consist of several pages. To navigate between pages, use the corresponding buttons in the middle of the quick button panel.
3. To enter a particular block, double-click on the corresponding symbol in the diagram.
4. To see the parent diagram, use the corresponding quick button in the middle of the quick button panel. Consult the Telelogic Tau documentation for more information about using the SDL Editor.

Summary

In this exercise we demonstrated how to use the Telelogic SDL Editor to inspect the automatically synthesized SDL model.

SDL diagrams in this exercise demonstrated the key points of the MSC to SDL mapping used by the KLOCwork MSC to SDL Synthesizer:

• Each MSC actor is mapped onto a separate SDL process
• All SDL processes are placed into a single SDL block
• If two MSC actors communicate, the corresponding SDL processes have a signalroute between them. The list of signals in this signalroute contain automatically generated signals corresponding to all possible messages between these two actors.
• A complete SDL process graph is synthesized for each SDL process.
• Definitions of signals are automatically generated.
• Data definitions are automatically generated.

In the following exercise we will show how to use Telelogic Tau to simulate the synthesized SDL for the InfoServer model. In the subsequent sections we will show how to use Telelogic Tau to perform automatic state space exploration on the synthesized SDL model in order to do an in-depth validation of the behavior input HMSC model.