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
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 waitparmresp, 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