CAV 2014 Measurements

↓ To the results ↓

On this page we provide all of our measurements comparing some state-of-the-art model checkers to our algorithm. The tools and algorithms included in the measurements are the following:

• NuSMV2: traditional BDD-based fixed point computations,
• NuXMV (NuSMV3): the newest generation of SAT-based model checking algorithms (so-called IC3), various abstraction and reduction techniques,
• ITS-LTL: the newest variant of saturation based model checking algorithms based on different automaton representations and optimizations,
• Hybrid MC: the prototype of our algorithm presented in the submitted paper currently implemented in C#.

The models are traditional asynchronous benchmark models [1,2]. In addition we used an industrial case-study of a safety logic in a nuclear power plant from [3]:

• Counter models a simple binary N-bit counter.
• The Round Robin model (RR-N)  is a resource sharing protocol and Slotted Ring (SR-N)  is the model of a communication protocol with N participants.
• DPhil is the well-known dining philosophers model.
• The Flexible Manufacturing System (FMS-N) and Kanban models a production system. The parameter N refers to the complexity of the model checking problem.
• PRISE example is a small, but important safety-critical industrial system: the safety function initiating an emergency procedure in a nuclear power plant. As verification requirement we used a complex fairness property stating that the initialization can be infinitely often activated under dangerous situations.

The following table shows the different models and expressions we evaluated in each tool, with the runtimes of the algorithms. To reproduce our results, one may download the following archives, in which we give our models, expressions and scripts, in some cases together with the tool itself. To run measurements in PetriDotNet, please refer to the README file in the Application folder. The other tools are run using the "run-timeout.bat" or "run_timeout.sh" script files. Be aware that NuSMV and NuXMV may require installation and modification of environment variables.

WARNING: The following packages contain executables in order to provide a way to exactly reproduce results, use them only for this purpose. If you need any of the tools for other use, the newest versions are available from their official websites with the proper licensing (all of them are free for personal and academic use).

• Measurement package for NuSMV (Linux, Win64)
• Measurement package for NuXMV (Linux, Win32)
• Measurement package for ITS-LTL (Win64)
• Measurement package for PetriDotNet (Hybrid MC, Win64, .Net4.0)

All measurements were done on a laptop with Intel^® Core™ i3-350M CPU (3M Cache, 2.26 GHz), 8 GB 1333 MHz DDR3 RAM, and a Samsung 840 EVO SSD. ITS and Hybrid MC were run on Microsoft Windows 8, while runtimes of NuSMV and NuXMV were measured on Ubuntu 13.10.

Memory consumption is not measured, as Hybrid MC is run in a managed environment (.Net), and the garbage collection mechanism could make the measurements not reproducible (memory consumption highly depends on the schedule of the GC). Experiments showed that Hybrid MC uses only a small amount of memory (despite it is run in a managed environment), and ITS-LTL is also efficient in terms of memory usage. NuSMV and NuXMV both has problems with memory, since they need to transform the input model to a low-level formalism, while Hybrid-MC and ITS both work on high-level models. Comparison to these tools is justified by the fact that they are well-known tools with stable algorithms, and highly poopular on the market.

Due to the limited precision of measurements, runtimes less than 0.01 are just signed "<0.01". Timeout was set to 1200s, cases where algorithms did not finish within this time limit are denoted by ">1200.00". When an algorithm ran out of memory, the table shows "memory" instead of the runtime. The sign "---" marks cases where the conversion of benchmark models to the tool's format was not done due to technical reasons (such as format incompatibilities, the size of the resulting model, or simply the fact that model checking of smaller models with the corresponding tool already failed to complete).

SCC detection statistics show some information about the performance of our hybrid approach. FP denotes the number of incremental symbolic fixed point computations actually started. R shows how many such computations were prevented by observing recurrent states, while A shows the same for explicit runs on abstractions.

¹ Runtime of the algorithm, total runtime with loading and conversion time shown in parentheses.

² Runtime results provided by the tool itself.

³ Runtime of state space exploration and model checking, total runtime with initialization and the building of the property automaton is shown in parentheses.

⁴ Order of applying these techniques is the following: (non-empty state and transition set) → (presence of accepting states) → presence of recurrent states → explicit search in the abstraction → incremental symbolic fixed-point computation. This way, the shown metrics mark cases where the technique was actually applied and broke the chain.

[1] Model Checking Contest: http://mcc.lip6.fr/models.php

[2] G. Ciardo, R. Marmorstein, and R. Siminiceanu. Saturation unbound. In Proc. Tools and Algorithms for the Construction and Analysis of Systems (TACAS 2003), LNCS 2619, pages 379-393. Warsaw, Poland, Apr. 2003. Springer-Verlag.

[3] Tamás Bartha, András Vörös, Attila Jámbor, Dániel Darvas: Verification of an Industrial Safety Function Using Coloured Petri Nets and Model Checking. In: 14th International Conference on Modern Information Technology in the Innovation Processes of the Industrial Entreprises (MITIP 2012), pp. 472-485, Budapest, Hungary, 10/2012.