BDD-Based Software Verification Applications to Event-Condition-Action Systems
Abstract
In software model checking, most successful symbolic approaches use predicates as representation of the state space, and SMT solvers for computations on the state space; BDDs are often used as auxiliary data structure. Although BDDs are applied with great success in hardware verification, BDD representations of software state spaces were not yet thoroughly investigated, mainly because not all operations that are needed in software verification are efficiently supported by BDDs.
We evaluate the use of a pure BDD representation of integer values, and focus on a particular class of programs: event-condition-action (ECA) programs with limited operations. A symbolic representation using BDDs seems appropriate for ECA programs under certain conditions. We configure a program analysis based on BDDs and experimentally compare it to four approaches to verify reachability properties of ECA programs: an explicit-value analysis, a symbolic bounded-loops analysis, a predicate-abstraction analysis, and a predicate-impact analysis. The results show that BDDs are efficient for a restricted class of programs, which yields the insight that BDDs could be used selectively for variables that are restricted to certain program operations (according to the variable's domain type), even in general software model checking. We show that even a naive portfolio approach, in which after a pre-analysis either a BDD-based analysis or a predicate-impact analysis is performed, outperforms all above-mentioned analyses.
An earlier version was published in Proc. MEMICS’12; the supplementary web-page of that version has been moved here.
Verification Tasks
A verification task is a pair consisting of a program and a property to check.
An archive with all programs that were considered for our experiments can be found here. These 46 programs were taken from the RERS challenges 2012 and 2013 (see the website of the competition).
Each property to check is represented by an error label within a program (reaching the label would mean that the property is violated). Each program contains 60 error labels (error_[0-59]), i.e., 60 properties to check. This sums up to 46 * 60 = 2760 verification tasks.
Experimental Results
Detailed results for the separate verification tasks are provided in form of a set of CSV files. The following files can be found within the archive:
| CSV file | Analysis |
|---|---|
| report-bdd-10gb.csv | BDD |
| report-bddimp-10gb.csv | BDD + Predicate Impact |
| report-bmc-10gb.csv | Bounded Loops (BMC) |
| report-ea-10gb.csv | Explicit Value |
| report-pa-10gb.csv | Predicate Abstraction |
| report-impact-10gb.csv | Predicate Impact |
Reproducing the Results
1. Check the Requirements
Before you can start to reproduce the results you have to make sure that following requirements are met:
- Linux operating system (the SMT solver used by CPAchecker, MathSAT5, is only available for Linux)
- Java JDK 1.7 (we used OpenJDK 1.7.0_55)
- 16 GB of RAM (or at least 8 GB, which would lead to different results)
2. Get (and build) CPAchecker
CPAchecker is free software; it is licensed under the Apache 2.0 Licence. The subversion repository with the source code is publicly available an can be found here here. We assigned the subversion tag cpachecker-1.3.4-sttt14 to the version of CPAchecker that we have used for our experiments. To reproduce the results you can either build CPAchecker from the source code (repository), or you can use a compiled version of it.
To use the compiled version of CPAchecker you just have to download the archive (click here for the download) and extract it.
To build CPAchecker from the source-code repository, you first have to checkout a copy. Run the following command to checkout the revision (that has been used for our experiments) from the repository:
svn co https://svn.sosy-lab.org/software/cpachecker/tags/cpachecker-1.3.4-sttt14/Build CPAchecker by running the command ant jar within the CPAchecker directory.
The CPAchecker directory should now contain all files that are necessary to run CPAchecker. It must contain at least the sub-directories "config", "scripts", and "lib". Beside that the file "cpachecker.jar" should exist. The next steps are explained starting from this directory (you should "cd" into it).
3. Choose the Verification Task
In this step you have to choose the verification task, i.e., you have to decide what property of what program to check.
CPAchecker uses monitor automata to specify the property to check. Since the properties to check are encoded in form of 60 error labels, there are 60 different automata (one for each error label). You can download this automata here (this archive contains the files error_[0-59].spc which correspond to the error labels; extract them to the folder "specs" within the CPAchecker directory).
Let's assume, that you want to verify whether the label error_33 of Problem3.c (taken from the suite of benchmark programs; extracted to the sub folder "programs" of the CPAchecker directory) can be reached.
4. Choose the Configuration
Before we can run CPAchecker on a verification task, we have to choose what analysis to run, i.e., what configuration parameters to use. The following table shows the configuration parameters that we used in our experiments for each analysis:
| Analysis | Configuration |
|---|---|
| BDD |
-bddAnalysis |
| BDD + Predicate Impact |
-combinations-bdd+impact |
| Bounded Loops (BMC) | -bmc-100 |
| Explicit Value | -explicitAnalysis |
| Predicate Abstraction | -predicateAnalysis-PredAbsRefiner-ABEl |
| Predicate Impact | -predicateAnalysis-ImpactRefiner-ABEl |
5. Run CPAchecker for one Verification Task
Now you should have a prepared your copy of CPAchecker, and decided what configuration to run on what verification task. For the following example, we assume that you decided to run a BDD analysis to verify whether the label error_33 of the program Problem3.c can be reached.
You can now run CPAchecker on the verification tasks using the following command:
./scripts/cpa.sh -heap 20000m -noout \
-bddAnalysis -setprop bdd.initBddNodeTableSize=200000000 \
-setprop bdd.bddCacheSize=2000000 \
-spec ./specs/error_33.spc ./programs/Problem3.c
The parameter -heap 20000m specifies the maximum amount of Java heap to allocate by the JVM; this only works for machines with sufficient (32 GB) RAM; you have to reduce this for your machine (for example, 10000m if your machine has 16GB of RAM installed).
The result should look similar to this:
Using the following resource limits: CPU-time limit of 900s (ResourceLimitChecker.fromConfiguration, INFO) CPAchecker 1.3-svn (OpenJDK 64-Bit Server VM 1.7.0_55) started (CPAchecker.run, INFO) Starting analysis ... (CPAchecker.runAlgorithm, INFO) Stopping analysis ... (CPAchecker.runAlgorithm, INFO) Verification result: TRUE. No property violation found by chosen configuration. More details about the verification run can be found in the directory "..."