Directed Model Checking for B: An Evaluation and New Techniques - Formal Methods: Foundations and Applications - page 12

A Experimental Results

Note: we use geometric mean [8] of the relative runtimes, as the arithmetic mean
is useless for normalised results. Of course, the geometric mean itself should also
be taken with a grain of salt (various articles also attack its usefulness). Indeed,
without knowing how representative the chosen benchmarks are for the overall
population of B specifications, we can conclude little.
Thus, we also provide all numbers in the tables below, so that minimum,
maximum relative runtimes can be seen, as well as the absolute runtime of the
reference benchmark. Indeed, the relative runtimes are less reliable, when the
absolute runtime of the reference benchmark is already very low. When a given
technique failed to locate the invariant violation (respectively deadlock or target
goal), then we have marked the time with two asterisks (**). The tables for the
models without errors where the full state space has to be explored can be found
in [18].

Table 1. Relative times for checking models with invariant violations (DF/BF)

Invariant Benchmark DF DF75 DF50 DF33 (abs+rel) DF25 Rel BF

SchedulerErr 0.33 0.33 0.33 30 ms 1.00 1.00 2.67

Simpson4Slot 163.33 0.22 0.67 90 ms 1.00 0.78 2.11

Peterson err 0.08 0.08 0.22 360 ms 1.00 3.06 11.17

TravelAgency 0.16 0.27 0.10 630 ms 1.00 0.78 2.43

SecureBldg M21 err3 0.50 0.50 1.00 20 ms 1.00 1.00 1.00

Abrial Press m2 err 0.26 3.38 0.34 880 ms 1.00 1.81 1.26

SAP M Partner 0.58 1.08 1.00 120 ms 1.00 0.92 0.83

NastyVending 0.02 0.08 8.00 130 ms 1.00 2.85 1.00

NeedhamSchroeder 1.28 1.52 0.95 22620 ms 1.00 0.70 1.37

Houseset 0.05 0.06 0.22 2610 ms 1.00 2.66 ** 336.27

BFTest ** 15000.00 11592.75 0.75 80 ms 1.00 1.00 0.88

DFTest1 0.20 0.35 0.71 2360 ms 1.00 1.01 1.02

DFTest2 7.86 0.50 0.60 2930 ms 1.00 0.99 1.00

GEOMEAN 1.03 0.78 0.58 394 ms 1.00 1.24 2.35