Action Language Verifier and
Composite Symbolic Library
7/7/2005 Release
Available at: http://www.cs.ucsb.edu/~bultan/composite/
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
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.