Validate the extended Server model

In this exercise we use the Telelogic Validator to perform automatic validation of our modified Server model.

1. Run KLOCwork MSC to SDL Synthesizer to synthesize the SDL model from the updated HMSC model.



2. Select the synthesized SDL system symbol.
3. Select the correct validation kernel. From the Organizer Generate menu, choose Make. The SDL Make window opens.
4. Select the Use Standard Kernel option in the Compile & Link options panel and select the appropriate validation kernel from the pull-down list. (The kernel should match the C/C++ compiler installed at your machine.) Then, click the Set button.



Prepare the Telelogic Validator and start the Validator UI by selecting the synthesized SDL system symbol and clicking the Validate quick button in the Tau Organizer.



The Validator UI starts.



5. Click the Exhaustive button to start the exhaustive state space exploration of the InfoServer model.

The Telelogic Validator tool analyzes the InfoServer model and produces validation reports. The reports are grouped into several categories. They include:

• 1 deadlock report
• 6 output reports
• 2 loop reports

Let's examine these reports.

The Telelogic Report Viewer lets you expand and collapse groups of reports in the tree.

The following figure shows a validation report for our InfoServer model, produced by the Telelogic Validator using the automatically synthesized SDL model.



6. To investigate the first report, expand the deadlock report and double click on the report symbol (saying Deadlock, Depth: 5). The Report Viewer tool starts the MSC Editor to show the trace of events, illustrating the abnormal behavior reported by the Validator.



7. Let's investigate the problems reported by the Validator. The first problem is a deadlock that happens when the User sends Init signal to the Server and then decides to enter the state A_LOOP_0, where it waits for a Failure signal (Failure scenario) from Server, while the Server at the same time enters the state A_LOOP_0, where it waits for Request or Done signals from the User instance. None of them are scheduled for transition.

The second problem is a failed output that happens when the User sends Init signal to the Server and then tries to perform the Done request (Request_Done scenario), while the Server at the same time decides to fail and sends the Failure message to the User. From observing the input scenarios is obvious that the User is not prepared to handle the failure of the Server when it has already committed to the Request_Done scenario.

Summary

In this exercise, we used the Telelogic Tau Validator to perform automatic validation of our modified Server model.

In the next exercise, we will fix the problem in the extended InfoServer model and perform another round of automatic validation.