Fix the problem and revalidate the MSC model

In this section we fix the problem in the extended InfoServer model and perform another round of automatic validation to verify that the problem is gone and no new problems were introduced.

Setup

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

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

In order to fix the problem discovered by the automatic state space exploration technique used by the Telelogic Tau Validator, let's introduce a delay into the User actor so that it checks that the Server has not failed. The User then expects the Failure signal from the Server before sending any requests to it. The delay should be introduced into the Request_done scenario (as shown in the following figure).

The delay should also be introduced into the Request_Data diagram (as shown in the following figure).

If the Server fails during the wait period, the User will disengage itself from further interactions with the Server (as shown in the following figure).

1. Save the updated Server model before performing the validation.
2. To perform the validation of the updated Server model do the following operations.
3. Synthesize the SDL model.
4. Check that the correct validation kernel is selected.
5. Select the synthesized SDL system symbol and start the Validator UI.
6. Select Exhaustive validation in the Validation UI. Now the Report Viewer offers only one report.



7. Let's examine the remaining problem. Click on the symbol Deadlock Depth: 5 in the Report Viewer. The Validator opens the MSC Editor and shows the sequence of events leading to this problem.



The MSC diagram describes the situation in which the Failure signal from the Server process arrives during the wait period of the User process. The User then disengages itself from the Server by leaving the a_loop state. The Server terminates (according to the MSC failure). This is the intended behavior. The Validator flags this situation as a deadlock because the process set of the synthesized system shows no further progress. The process User is now in a loop (state failure_2) and no further messages can force the Server process to leave this state. From the SDL perspective, this is a deadlock. However, from our modeling perspective, this deadlock is insignificant because, according to our input MSC model, the behavior of the system is undefined after we finish all the explicitly specified scenarios and reach the HSMC termination symbol.

To break the deadlock discovered by the Validator, we should extend the input specification of the Server and decide what the expected behavior of the User actor should be after the Server fails. One potential solution is to terminate the User actor in this situation.