Information Technology Reference
In-Depth Information
Table 2. Relative times for checking models with deadlocks (DF/BF Analysis)
Deadlock Benchmark
DF DF75 DF50 DF33 (abs+rel) DF25 Rel
BF
Abrial Earley3 v3
0.33
0.44
0.93
270 ms 1.00
1.19
1.19
Abrial Earley3 v5
0.13
0.32
0.75
4320 ms 1.00
2.18
7.95
Abrial Earley4 v3
0.89
0.89
1.00
90 ms 1.00
1.00
1.00
Alstom axl3
0.10
0.17
0.20 51270 ms 1.00
3.51
14.61
Alstom ex7
** 4.20
0.23
0.35 856320 ms 1.00
** 1.21 ** 3.00
Bosch CrsCtl
1.00
1.00
1.00
3ms1.00
4.00
4.00
SAP MChoreography
0.50
0.50
0.50
20 ms 1.00
1.00
1.00
DiningPhil
0.13
0.26
0.36
1690 ms 1.00
2.49
6.20
CXCC0
0.50
1.00
1.00
10 ms 1.00
2.00
2.00
GEOMEAN
0.43
0.44
0.59
540 ms 1.00
1.82
3.02
AVG
0.00
0.00
0.00
0ms0.00
0.00
0.00
Table 3. Relative times for checking models with goals to be found (DF/BF Analysis)
Goal Benchmark
DF DF75 DF50 DF33 (abs+rel) DF25 Rel BF
RussianPostal
0.95
0.14
0.73
220 ms 1.00
1.05 1.50
TrainTorch
1.14
1.17
0.69
350 ms 1.00
1.06 0.94
BlocksWorld
0.07
0.25
1.16
440 ms 1.00
1.18 1.07
Farmer
0.50
1.00
0.50
20 ms 1.00
1.00 1.00
Hanoi
0.54
0.48
1.00
500 ms 1.00
0.84 0.90
Puzzle8
7.56
2.86
0.40 59060 ms 1.00
0.11 0.71
RushHour
0.41
0.66
0.90 127020 ms 1.00
1.09 1.11
Abrial Press m13
899.78
1.64
1.26
800 ms 1.00
0.66 2.23
Abrial Queue m1
1.60
3.00
1.00
50 ms 1.00
1.60 1.40
SystemOnChip Router
0.05
0.14
0.08
2050 ms 1.00
1.04 1.45
Wegenetz
0.08
0.08
0.25
120 ms 1.00
0.17 2.58
GEOMEAN
0.92
0.57
0.58
715 ms 1.00
0.71 1.26
Table 4. Relative times for checking models with invariant violations (Heuristics)
Invariant Benchmarks DF33 (abs+rel) HashRand OutDegree OutDegHash TermSi ze
SchedulerErr
30 ms
1.00
0.33
3.67
10.67
2.67
Simpson4Slot
90 ms
1.00
0.89
2.22
0.78
2.22
Peterson err
360 ms
1.00
0.75
11.25
1.42
9.14
TravelAgency
630 ms
1.00
0.52
1.02
9.98
0.49
SecureBldg M21 err3
20 ms
1.00
0.50
1.00
0.50
0.50
Abrial Press m2 err
880 ms
1.00
1.45
3.38
3.19
1.25
SAP M Partner
120 ms
1.00
1.17
0.75
0.33
1.00
NeedhamSchroeder
22620 ms
1.00
1.40
**48.51
41.58 ** 46.06
Houseset
2610 ms
1.00
0.08 ** 333.53
0.16 ** 338.61
BFTest
80 ms
1.00
16.00
0.88
73.00
0.88
DFTest1
2360 ms
1.00
0.64
1.02
0.69
1.02
DFTest2
2930 ms
1.00
0.53
1.00
0.57
1.66
GEOMEAN
432 ms
1.00
0.79
2.44
1.54
1.93
Previous Page
Next Page
Formal Methods: Foundations and Applications
Search WWH ::




Custom Search
Home