
Automated Statistical Testing for Embedded Systems 121
TABLE 5.2 (Continued)
Example Usage Models, One Structure, Two Matrices of Transition Probabilities
From-State To-State Stimulus Uniform
Probabilities
Specific
Environment
8 Basal Running 8 Basal Running BD 1/8 0.10
8 Basal Running 14 Bolus Running BG 1/8 0.20
8 Basal Running 15 Alarm2 AL2 1/8 0.05
8 Basal Running 16 EXIT POFF 1/8 0.05
8 Basal Running 16 EXIT TIF 1/8 0.05
9 Bolus
Alarm-Empty
10 Bolus
Drug-notOK
DNOK 1/3 0.30
9 Bolus
Alarm-Empty
14 Bolus Running DOK 1/3 0.60
9 Bolus
Alarm-Empty
16 EXIT POFF 1/3 0.10
10 Bolus
Drug-notOK
10 Bolus
Drug-notOK
DNOK 1/3 0.30
10 Bolus
Drug-notOK
14 Bolus Running DOK 1/3 0.60 ...