Siêu thị PDFTải ngay đi em, trời tối mất

Thư viện tri thức trực tuyến

Kho tài liệu với 50,000+ tài liệu học thuật

© 2023 Siêu thị PDF - Kho tài liệu học thuật hàng đầu Việt Nam

Validation of Communications Systems with SDL phần 7 ppt
MIỄN PHÍ
Số trang
28
Kích thước
266.9 KB
Định dạng
PDF
Lượt xem
1180

Validation of Communications Systems with SDL phần 7 ppt

Nội dung xem thử

Mô tả chi tiết

Random Simulation 173

Figure 6.5 Adding the stop condition

6.3.1.2 Analyze the error

To understand the bug, you will search in which state process dispatch was (in block dlcb)

when process DLC transmitted to it the signal dlcstopped.

A. In the Simulator, press the button Watch and select States: a watch appears, shown in

Figure 6.6, displaying the state of each process instance. You see that process dispatch in

block dlcb is in state waitparmresp.

Figure 6.6 The watch window

B. In the Editor, open the partition part1 of process dispatch: you see that in state waitparm￾resp, the only input is L SetParmResp; therefore, when a v76frame is first in the process

queue, it is discarded.

If required, the MSC trace corresponding to the bug can be generated by pressing the buttons

Start MSC, undo and then redo .

We will not correct this bug, because we will learn how to find it with exhaustive simulation.

174 Validation of Communications Systems with SDL

6.3.2 Multiple random simulations

The random simulation algorithm used in the Simulator is based on a pseudorandom number

called seed. The initial default seed value (619430284 in the version used) can be changed

using Edit > Configuration. At each random simulation step, the Simulator:

• executes a transition selected among the firable transitions according to the current seed

value, (for example, if there are two firable transitions, depending on the seed value, the first

or the second transition is executed),

• computes the new seed value function of the current seed value.

It means that the seed changes at every simulation step. Also, if you go back (undo or init

commands) to previous simulation steps, seed does not return to its previous value: this is to

simulate different branches easily. Otherwise, using the same seed from the same model’s state

would simulate the same scenario.

To illustrate this:

A. Quit the Simulator, start the Simulator as indicated in Section 6.3.1.1 and enter the stop

condition rstep = 500 .

B. Press on to start the random simulation: at Step 261 (you may get another number), the

simulation stops (unexpected signal).

C. Press on init , four times on redo and then on : this time, the simulation stops at

Step 264 (you may get another number).

D. Repeat the same sequence: this time, the simulation stops at Step 48 (you may get

another number).

The fact that the random simulation starting from the same SDL model state stops at

Step 261, 264 or 48 means that different scenarios have been simulated, because the seed

was always different (computed at every step, then never reinitialized during init).

To automatically perform the previous random simulations, we are going to write a script.

E. With a text editor, type the following lines and save the file as rand.wri:

init -- return to step 0

source start.scn -- execute the 4 start

untrace all -- remove textual traces

define trace_stmt ’false’ -- remove PR traces

-- Protection against double declaration of sim_ok:

if ’$vars_declared’ = ’’

define vars_declared ’Yes’

dcl sim_ok Boolean

fi

let sim_ok = true

while sim_ok

Tải ngay đi em, còn do dự, trời tối mất!