Validation of Communications Systems with SDL phần 5 potx

114 Validation of Communications Systems with SDL

obs_1

sigA

sigC

inst_dlca

DLCa

sigB

Figure 5.4 The observer MSC obs 1

of the MSC to verify: in this case, the Simulator will not explore the states leading to an

error (a violation) of the MSC, because the default configuration is error cut (equivalent to

prune in Tau).

5.2 CASE STUDY WITH TAU SDL SUITE

In Chapter 4, we have used the Tau SDL Suite Simulator. To benefit from automatic observation

features, we will now switch to the Tau SDL Suite Validator. Note that the Simulator can also

be used to check the SDL model against an MSC.

5.2.1 Simulate with user-defined rules

In the Validator, only one user-defined rule can be used at a time. To check several conditions,

you can use the operator or to group them in a single rule.

5.2.1.1 Detect DLC establishment

We want to detect that a DLC is established. This means, in our V.76 SDL model, that:

• instance 1 of process DLC in block DLCa is in state connected, and

• instance 1 of process DLC in block DLCb is in state connected.

It seems that the Validator rules do not accept qualifiers such as <<Block DLCa>>. As

there are two processes named DLC, one in block DLCa and the other in block DLCb, it is not

possible to write a rule to detect that both DLCs are in state connected. An observer process

could be used instead.

The solution would be to modify the SDL model to have a copy of block V76 DLC on each

side: transformation of the block type V76 DLC into a block named V76a, making a copy of it

and naming the copy V76b and in each block, renaming the DLC process, respectively, DLC a

and DLC b. Then, the Validator user-defined rule would be:

state(DLC_a:1)=connected and state(DLC_b:1)=connected

Rather than performing this model modification, you will use rules concerning process AtoB

and BtoA, which do not require the use of qualifiers, as they are unique in the system.

Automatic Observation of Simulations 115

5.2.1.2 Detect state of processes AtoB and BtoA

We want to detect that in our V.76 SDL model:

• instance 1 of process AtoB is in state ready and

• instance 1 of process BtoA is in state ready.

This condition, translated into a Validator rule, becomes:

state(AtoB:1)=ready and state(BtoA:1)=ready

Compile the SDL model, start the Validator and test the rule:

A. In the Organizer, select the SDL system V76test and do Generate > Make: the window

represented in Figure 5.5 appears. Select Microsoft Validation or Borland Validation, and

press Full Make.

Figure 5.5 The SDL Make window set for validation

B. In the Organizer, press the Validate button to start the Validator. The Validator main

window appears, as shown in Figure 5.6.

C. In the Validator command line, enter:

Define-Rule state(AtoB:1)=ready and state(BtoA:1)=ready

D. Then, to test if the rule is satisfied or not for the current SDL model state, enter:

Evaluate-Rule state(AtoB:1)=ready and state(BtoA:1)=ready

116 Validation of Communications Systems with SDL

Figure 5.6 The Validator main window

The Validator answers:

Evaluating rule:

(( state( AtoB:1 ) = ready) and (state( BtoA:1 ) = ready ))

Rule not satisfied

This is normal, as the processes are not yet in state ready.

E. Select View > Command Window: you see that the processes AtoB:1 and BtoA:1 are in

state start.

F. Press the Navigator button. In the Navigator window, double-click two times on Next 1 to

execute the start transitions of AtoB and BtoA, as shown in Figure 5.7.

Figure 5.7 Starting processes AtoB and BtoA