The BEEM Database

There are several problems with the development of a standard approach. Different verification tools (such as Spin, SMV, Murphi, or Uppaal) are typically designed for very specific domains of problems that do not always overlap. Spin, for instance, is designed for models of asynchronous software systems, SMV was designed primarily for the verification of hardware circuits, and Uppaal was designed primarily for real-time verification problems. Modeling a hardware circuit as a Spin model is typically not a good idea, as is the verification of a real-time asynchronous software verification problem in SMV.

Each verification tool tends to have its own specification format, and a specific set of primitives for which it can give optimized performance. Translation from one format into another is always plagued with the problem that an encoding that is efficient for one tool is translated into an encoding that is inefficient for another tool. An experienced user can in these cases typically come up with a new version of the converted model that performs significantly better than the default mechanically translated version.

The most meaningful tool comparisons that have been done to date, therefore, have involved the original designers of each verification tool to craft optimal encodings of the same basic model for each different tool. A comparison of the resulting tool performance, as used by expert users on the same verification problems now becomes a much better indication of a tool's relative strengths and weaknesses. Only a handful of such studies has been done to date.

Beem

The collection contains 57 separately models, categorized in 8 different groups (communication protocols, mutual exclusion algorithms, leader election algorithms, other protocols, controllers, planning and scheduling, puzzles, and miscellaneous).

Each model is parameterized to yield between 3 and 8 different problem instances, which brings the total number of models in the database to 298. For each instance there is a wealth of information provided in the database.

Most, though not all, models in the database have both a version in a basic DVE format that supports the DiVinE Distributed Verification Environment toolset, together with a small number of relevant correctness properties. For many, though not all, model instances there is also a mechanically generated Promela version of the model, that can be verified with the Spin tool. At the time of writing (March 31, 2007) we counted 232 of the 298 models as having a Spin version. The Spin versions are not in all cases comparable to the DVE version (as measured by the number of reachable states), but in quite a few cases they are.

We downloaded all 232 Spin models, and the statistics on the verification performed with the DiVinE toolset (as available in xml files for some of the problem instances, or from the main pages for each model). We then setup a test-script to run verifications for each of the models, with settings that should be roughly comparable to those used for the DiVinE tests. Specifically: we ran the tests on a 64-bit Linux workstation with 8 GB of memory, running at 2.3 GHz. The verification settings were as follows (note that we use the default 64-bit compilation which can increases memory use):

	#!/bin/sh

	echo Safety Verification
	for i in *.pm
	do	echo $i
		spin -a $i > stderr/$i 2>&1
		cc -O3 -DSAFETY -DMEMLIM=7000 -DNSUCC -o pan pan.c 2>> stderr/$i
		./pan -m10000000 -c0 -n -w27 > stdout/$i 2>> stderr/$i
	done

We list all models here in alphabetical order, rather than grouped in categories as in the BEEM database. None of the Spin versions of the models were modified from the mechanically generated versions in the BEEM database, with one exception. The exception is the production_cell example where a syntax error exists in the generated model: the name done is used as both a labelname and as a variable name in some of the problem instances. We have renamed the variable name into Done to avoid this problem. Clearly, rewriting the generated models could lead to huge reductions in complexity (e.g., by using channels instead of buffers) but we have resisted doing so.

In the table below, all results from Spin are given in blue, all results from the BEEM database are in red. Where one of the two tools performed better (in terms of given a shorter overall runtime without failing the run) the corresponding number is set in bold, red or blue. When no number from the BEEM database was present in the xml files, the corresponding field in the table has been left blank. A red or blue x in the last column indicates that BEEM or Spin did not complete the search, either by exhausting the maximum stack depth or by exhausting the maximum amount of available memory.

At the bottom of the table some statistics are generated for the relative performance of the BEEM and Spin verifications (where comparisons were possible).

One of the objectives of the BEEM database is to facilitate evaluating the performance of multi-core algorithms for model-checking. We have not done multi-core performance tests with Spin yet for these models (and none are present in the BEEM database for DiVinE yet either), but we plan to add these later.

Stats (unmodified Spin models as mechanically generated from DVE format):
Nr of cases where Spin failed: 42 of 232 fraction: 0.181034
Nr of cases where Beem failed: 38 of 232 fraction: 0.163793
Nr of cases where Spin has shorter runtime: 166 of 232 fraction: 0.715517
Nr of cases where Beem has shorter runtime : 33 of 232 fraction: 0.142241
Nr of cases where Spin has fewer states: 79 of 232 fraction: 0.340517
Nr of cases where Beem has fewer states: 107 of 232 fraction: 0.461207
Nr of cases with matching nrs of states : 13 of 232 fraction: 0.0560345
Nr of cases with matching nrs of states +- 10%: 105 of 232 fraction: 0.452586
Nr of cases where Beem has fewer states but a longer runtime: 107 of 107 fraction: 1

generated: Sun Apr 1 19:35:35 PDT 2007
BEEM database
Spin homepage