Validation of Communications Systems with SDL phần 9 pptx

232 Validation of Communications Systems with SDL

A. In the Simulator, press on the button Verify...

B. In the Verifying window, press on Limit a queue...

C. In the Limit a queue window, press on Instance.

D. In the Instance window, select process atob(1) and press OK.

E. In the Limit a queue window, press on Apply.

F. Repeat the previous steps for instances btoa(1), dlca!dispatch(1) and dlcb!dispatch(1).

G. Check that the list filter command gives the results below:

> list filter

filter is_active(dlcb!dispatch(1)) and length(dlcb!dispatch(1)

! queue) > 1

filter is_active(dlca!dispatch(1)) and length(dlca!dispatch(1)

! queue) > 1

filter is_active(btoa(1)) and length(btoa(1) ! queue) > 1

filter is_active(atob(1)) and length(atob(1) ! queue) > 1

H. We need filters for process instances DLC(1) and DLC(2), in blocks DLCa and DLCb.

Select Edit > Filter Conditions and add the following filters:

is_active(dlca!dlc(1)) and length(dlca!dlc(1)!queue) > 1

is_active(dlcb!dlc(1)) and length(dlcb!dlc(1)!queue) > 1

is_active(dlca!dlc(2)) and length(dlca!dlc(2)!queue) > 1

is_active(dlcb!dlc(2)) and length(dlcb!dlc(2)!queue) > 1

We must also limit the number of instances that can be created, because each new process

instance gets its own new Pid; therefore, each new Pid generates a new global state. For

example, if you simulate 50 times the sequence ‘establish a DLC, release a DLC’, you get 50

different Pids for process DLC. Remember that the limit indicated in the SDL model such as

DLC(0, 2) only prevents having more than two instances of process DLC at the same time.

I. In the Simulator, select Edit > Filter Conditions and add the following filters:

create dlca!dlc(3)

create dlcb!dlc(3)

It means that the sequence ‘establish a DLC, release a DLC’ can be simulated two times only,

because the transition leading to the creation of the third instance of process DLC is filtered.

You can try the sequence in interactive mode, and see that after the sequence mentioned, it is

not possible to establish a new DLC (signal L EstabReq).

J. Finally, to simulate first a configuration where signals are not lost in the block dataLink,

add the following filters:

trans btoa(1) : decision_lose_the_frame(‘Yes’)

trans atob(1) : decision_lose_the_frame(‘Yes’)

Now the only answer to the decision ‘Lose the frame’ is ‘No’.

Exhaustive Simulation 233

7.4.4.3 Save and tune the filters

To avoid entering again the filters at the next simulation session, we will save them into a file,

automatically executed by the model startup file.

A. In the Simulator, type the command:

list filter >> v76_filter.wri

This creates the file v76 filter.wri and inserts the filter commands into it. We will simplify

the filters: as the instances of process dispatch, AtoB and BtoA are static, that is, always exist,

we can remove the expression is active before them.

B. Open the file v76 filter.wri and remove is active before dispatch, AtoB and BtoA. The file

should now contain:

filter length(atob(1) ! queue) > 1

filter length(btoa(1) ! queue) > 1

filter length(dlca!dispatch(1) ! queue) > 1

filter length(dlcb!dispatch(1) ! queue) > 1

filter is_active(dlca!dlc(1)) and length(dlca!dlc(1)!queue)

> 1

filter is_active(dlcb!dlc(1)) and length(dlcb!dlc(1)!queue)

> 1

filter is_active(dlca!dlc(2)) and length(dlca!dlc(2)!queue)

> 1

filter is_active(dlcb!dlc(2)) and length(dlcb!dlc(2)!queue)

> 1

filter create dlca!dlc(3)

filter create dlcb!dlc(3)

trans btoa(1) : decision_lose_the_frame(‘Yes’)

trans atob(1) : decision_lose_the_frame(‘Yes’)

C. Open the file v76.startup and add source v76 filter.wri. The file v76.startup should now

contain:

source v76_feed.wri

source start.scn

source v76_filter.wri

7.4.4.4 Set the configuration options

To get less global states, we will change the default settings of the Simulator. See Chapter 4

for details on Edit > Configuration.

A. Select Edit > Configuration and set Reasonable environment to on (box checked) and Loose

time progression to off (box not checked).

234 Validation of Communications Systems with SDL

7.4.4.5 Run the exhaustive simulation

In case the simulation never terminates, you can stop it by pressing the halt button.

A. Type the command verify to start the exhaustive simulation: the Simulator displays the

current options and starts the exhaustive simulation:

mode breadth

...

deadlock limit 2

exception limit 2

stop limit 2

define stop_cut true

define states_limit 20000

define depth_limit 0

...

define verify_stats true

Then, after every 8192 global model states, the Simulator displays a line showing the simula￾tion progression: number of (unique) global states, number of transitions executed, time elapsed

since the beginning of simulation, maximum depth reached in the states graph and maximum

breadth reached in the states graph.

(8192 states 11676 trans. 1 seconds, depth=34, breadth=934)

(16384 states 23502 trans. 2 seconds, depth=40, breadth=1615)

(24576 states 35716 trans. 4 seconds, depth=44, breadth=2086)

...

(65536 states 99823 trans. 12 seconds, depth=58, breadth=3269)

(73728 states 113177 trans. 14 seconds, depth=61, breadth=3269)

(81920 states 126678 trans. 15 seconds, depth=65, breadth=3269)

After 17 seconds, the exhaustive simulation stops and the Simulator displays the results:

Number of states : 87174

Number of transitions : 135912

Maximum depth reached : 79

Maximum breadth reached : 3269

duration : 0 mn 17 s

Number of exceptions : 0

Number of deadlocks : 0

Number of stop conditions : 0

Transitions coverage rate : 100.00 (0 transitions not covered)

States coverage rate : 100.00 (0 states not covered)

Basic blocks coverage rate : 92.98 (4 basic blocks not covered)

etc.

The simulation has covered all the 87174 reachable states of the reduced configuration of

our SDL model. Obtaining such a coverage of the behavior would take weeks of interac￾tive simulation.

No exceptions or deadlocks have been found.