Validation of Communications Systems with SDL phần 8 pps

Exhaustive Simulation 201

dispatch_4

process

<<Block DLCb>>

dispatch

dispatch_3

process

<<Block DLCa>>

dispatch

BtoA_2

BtoA

AtoB_1

AtoB

env_0

MSC bug_exh3

Removed beginning (47 messages)

DLC_7

waitUAdisc

/* Not yet consumed by */ dispatch_4

L_ReleaseReq

( 1)

L_DataReq

( 1, 39 ) L_DataReq

V76frame

( DISC : (. 1 .))

V76frame

( DISC : (. 1 .))

L_ReleaseReq

( 1)

DLC_7

process

<<Block DLCa>>

DLC

( 1, 39 )

Figure 7.23 Last steps of the error MSC trace

A. Exit from the Validator (answering No to the question).

B. In Windows (or Unix), make a copy of the file dlc.spr into dlc v5.spr.

C. In process DLC, page part2, insert a coma followed by L DataReq in the input containing

L ReleaseReq previously added, as illustrated in Figure 7.24.

D. Save the SDL model.

waitUAdisc

V76frame (V76para)

V76para ! present

UA, DM

DLCstopped(me)

ELSE

-

L_ReleaseReq,

-

L_DataReq

Figure 7.24 After adding input of signal L DataReq

7.3.3.3 Run the exhaustive simulation

A. In the Organizer, select the SDL system V76test and press the Validate button.

B. In the Validator, select Commands > Include Command Script, and choose sig defs.com.

C. Press on List Signal, and check that you get the same signals as previously.

D. In the Validator, select Options2 > Exhaustive: Depth and enter 30.

202 Validation of Communications Systems with SDL

E. Press on Exhaustive; the Validator displays:

** Starting exhaustive exploration **

Search depth : 30

** Exhaustive exploration statistics **

No of reports: 3

Generated states: 8425

Truncated paths: 1708.

Unique system states: 6856.

Size of hash table: 100000 (400000 bytes)

Current depth: -1

Max depth: 30

Min state size: 212

Max state size: 572

Symbol coverage : 90.55

The exhaustive simulation has stopped and found 6856 unique system states (note that more

states would have been found if the search depth was not limited to 30). The Report Viewer

appears, showing that the only reports are three MaxQueueLength: the default limit of three

signals in some process input queues has been exceeded. This is normal; more details are

provided later.

In the 6856 explored global states of the SDL model, we are sure that we have no errors and

no deadlocks. However, the global states not yet explored by the Simulator may contain errors.

7.3.4 Millions of states: detect output to Null

Now to test more features in the SDL model, we use a larger model configuration: again, one

signal maximum in each queue, but the maximum exploration depth is no longer limited. To

limit the number of states, we restrict the number of retransmissions in process DLC to 1,

instead of 3.

7.3.4.1 Limit number of signals in input queue

To avoid an infinite number of global states, we need to limit the number of signals present in

the input queue of each SDL process.

For example, in the V.76 SDL model, if you simulate the scenario shown in Figure 7.51,

the queue of the instance 1 of process DLC in block DLCa contains 4 signals. If this process

does not input the signals in its queue while other bursts of L DataReq are transmitted to

process dispatch, the number of L DataReq stacked in the queue will grow rapidly. In addi￾tion, each new signal stacked in the queue generates a new global SDL model state during

exhaustive simulation.

The Validator by default limits to three signals in each process instance input queue. To

reduce the number of states, we will limit to one signal in each queue; note that some models

might not work with such a limit, for example, if two signals are transmitted at the same time

to a process queue.

Exhaustive Simulation 203

7.3.4.2 Modify the SDL model

A. Exit from the Validator (answering No to the question).

B. Open process DLC part1 and replace 3 by 1 in the declaration of N320, to obtain:

SYNONYM N320 Integer = 1;

C. Save the SDL model.

7.3.4.3 Run the bit-state simulation

After trying exhaustive simulation, we have found that it required 416 MB of RAM for 406049

unique global states of the SDL model. In ObjectGeode, we use exhaustive simulation because

it compresses the global states (for example, storing once several identical input queues): in

only 196 MB of RAM, ObjectGeode stores 2620001 states of the same model.

This is why instead of using exhaustive simulation we will use bit-state. Bit-state mode is

similar to exhaustive mode, but it requires less memory, because instead of storing each new

global model state, bit-state stores only one bit in an array. The index in the array is a hash￾coding (a kind of checksum) of the global state contents. However, two different global states

may have the same hash-code: they are considered as identical, therefore parts of the states

graph may remain unexplored.

A. In the Organizer, select the SDL system V76test and press Validate .

B. In the Validator, select Options1 > Input Port Length, and enter 1.

C. Select Options2 > Bit State: Hash Size and enter 250000000 (250 millions of bytes). This

is the size of the array of bits used to store the states hash-codes. If your machine is

equipped, for example, with 128 MB of RAM, enter 80 millions.

D. Select Options2 > Bit State: Depth and enter 15000.

E. Select Commands > Include Command Script, and choose sig defs.com.

F. Press on List Signal, and check that you get the same signals as previously.

G. Press on Bit State, the Validator displays:

** Starting bit state exploration **

Search depth : 15000

Hash table size : 250000000 bytes

Transitions: 20000 States: 12408 Reports: 5 Depth: 376 Symbol

coverage: 93.60 Time: 10:07:07

Transitions: 40000 States: 24847 Reports: 5 Depth: 300 Symbol

coverage: 93.60 Time: 10:07:07

Transitions: 60000 States: 37274 Reports: 5 Depth: 138 Symbol

coverage: 93.60 Time: 10:07:07

...