Simulate system slice

In this exercise, we demonstrate how to use the KLOCwork MSC to SDL Synthesizer to produce slices of MSC models. An MSC slice contains a subset of all instances from the original MSC model.

Our Server model consists of two instances (User and Server). The original Server model was self-contained (no messages to or from the environment of the model). In the previous exercises, we introduced environment controls for the User instance, thus making the model open. However, the instance User became trivial. All the decision-making for this user is now done in the environment of the model. The User only passes the signals to the Server model. MSC slice allows us to eliminate the User instance and interact directly with the Server instance.

Setup

All source MSC PR files, Telelogic Tau diagrams, and the synthesized SDL model are found in the following directory:

<KLOCwork MSC to SDL installation directory> / doc/examples/InfoServer_step4

1. Copy the file msc2sdl.ini from the KLOCwork MSC to SDL Synthesizer installation directory to your working directory.

The file should have the following contents:

# comment

OPT_UPPERCASE=yes

OPT_ALL_WARNINGS=yes

OPT_CROSS_REFS=yes

OPT_CLEAN_GEN_PR = yes

2. Add the following two lines (shown in bold font) to the file.

GENERATED_SYSTEM_NAME = "Server"

SLICE = "Server"

The msc2sdl.ini file contains the options for the KLOCwork MSC to SDL Synthesizer. The GENERATE_SYSTEM_NAME option provides the name of the generated SDL model corresponding to the MSC slice. The SLICE option defines the list of MSC instances to be included in the MSC slice during the synthesis. For a complete description of KLOCwork MSC to SDL Synthesizer options, see the KLOCwork MSC to SDL Synthesizer Reference Manual.

3. Synthesize the SDL model that corresponds to the selected MSC slice. To do this, in the Telelogic Tau Organizer from the MSC to SDL menu, choose Synthesize plain SDL. The synthesized slice is placed into the Server module of the Organizer.



Observe that, in comparison to the complete generated SDL model, the slice contains only the SDL process SERVER. Note, also, that the synthesized SDL model has a different name (Server instead of the default name SynthesizedModel) as the result of setting the GENERATED_SYSTEM_NAME option.

4. Inspect the SDL model of the synthesized slice.



Observe that the synthesized SDL system Server has a channel to the environment. The list of signals for this channel corresponds to the interface of the Server instance according to the input MSC model.

5. From the MSC to SDL menu, choose Simulate MSC. Observe new synthesized buttons in the Simulator UI button panel. The synthesized buttons correspond to the input interface of the Server instance.



6. Click the MSC button in the Trace group, then start the simulation by clicking the Go button from the Execute group.
7. Explore the behavior of the Server by sending the following signals: Init, Request, Done. Observe the generated MSC trace.



8. Restart the Simulator UI. Click the MSC button and start the simulation by clicking the Go button.
9. Explore the abnormal behavior of the Server by sending the following sequence of signals: Init, Boo. Observer the generated MSC traced.



10. Restart the Simulator UI. Click the MSC button and start the simulation by clicking the Go button.
11. Explore the abnormal behavior of the Server by sending the following sequence of signals: Boo, Init. Observe the generated MSC traced.

Summary

In this exercise we demonstrated how to use the KLOCwork MSC to SDL Synthesizer to produce slices of MSC models.