Action Language Verifier and Composite Symbolic Library

7/7/2005 Release
Available at:
You can download the source code for the Action Language Verifier and the Composite Symbolic Library here: composite-0.4.tar.gz
You can download the executable for the Action Language Verifier for Linux PCs here: action-0.4.gz
Here are a set of Action Language specifications verified using Action Language Verifier: Examples

Project Descriptions and Related Publications

Action Language Verifier

Action Language is a specification language for reactive software systems. It supports both synchronous and asynchronous compositions and hierarchical specifications. An Action Language specification consists of integer, boolean and enumerated variables, parameterized integer constants and a set of modules and actions which are composed using synchronous and asynchronous composition operators. Action Language Verifier is an infinite state symbolic model checker which consists of 1) a compiler that converts action language specifications to composite symbolic representations, and 2) a model checker which verifies CTL properties of Action Language specifications. Action Language Verifier uses the Composite Symbolic Library as its symbolic manipulation engine. Our tool supports polymorphic verification procedures which dynamically select symbolic representations based on the input specification.

Since Action Language allows specifications with unbounded integer variables, fixpoint computations are not guaranteed to converge. Action Language Verifier uses conservative approximation techniques, reachability and acceleration heuristics to achieve convergence. Recent additions to Action Language Verifier include automated counting abstraction for verification of arbitrary number of finite state processes, and dependency analysis and marking heuristic for improving the efficiency of the fixpoint computations.

Composite Symbolic Library

Composite Symbolic Library combines different symbolic representations, such as BDDs for representing boolean logic formulas and polyhedral representations for linear arithmetic formulas, with a single interface. Based on this common interface, these data structures are combined using what we call a composite representation. Main idea is to use a disjunctive normal form where every disjunct consists of a conjunction of different symbolic representations. Using this idea we can represent each variable type with a suitable symbolic representation to improve the efficiency of symbolic model checking. In our tool, enumerated and boolean variables are represented by BDDs, and integer variables are represented with polyhedral representations.

We used an object-oriented design to implement the composite symbolic library. We imported CUDD (a BDD library) and Omega Library (a linear arithmetic constraint manipulator that uses polyhedral representations) to our tool by writing wrappers around them which conform to our symbolic representation interface. More recently, we integrated an automata representation for arithmetic constraints using the automata package of the Mona tool. (To use the Composite Symbolic Library you have to download and install these tools first.) Composite Symbolic Library also supports efficient representation of bounded arithmetic constraints using BDDs. Our symbolic representation library can form an interface between different symbolic libraries, model checkers, and specification languages. We expect our tool to be useful in integrating different tools and techniques for symbolic model checking, and in comparing their performance.

This material is based upon work supported by the National Science Foundation under Grants CCF-9970976 and CCF-9984822.