Tools Developed at VLab
Action Language Verifier and Composite Symbolic Library
Action Language is a specification language for reactive software systems that supports both synchronous and asynchronous compositions and hierarchical specifications. Action Language Verifier consists of 1) a compiler that converts Action Language specifications to composite symbolic representations, and 2) an infinite state model checker which verifies CTL properties of Action Language specifications.
Composite Symbolic Library is a symbolic manipulator for automated verification which combines different symbolic representations using an object oriented design. Currently, Composite Symbolic Library supports BDDs for representing boolean logic formulas, and polyhedral and automata representations for linear arithmetic formulas. An extension to Composite Symbolic Library implements shape analysis for checking properties of linked lists.
Web Service Analysis Tool
A tool for analyzing interactions among web services. It consists of: 1) An intermediate representation for web services which supports XML data manipulation; 2) Synchronizability analysis which determines if the asynchronous communication among web services can be synchronized without changing their interaction pattern; 3) Realizability analysis which determines if an interaction pattern can be realized by asynchronously communicating web services; 4) Translators from a subset of BPEL to the WSAT intermediate representation and from the WSAT intermediate representation to Promela, input language of the SPIN model checker.
NetStub
NetStub is a framework for verification of distributed Java Applications. It is based on a set of stub classes that replace native methods used in network communication and enables verification of distributed Java applications by isolating their behavior from the network. The framework supports two modes of verification: unit verification and integration verification. Integration verification checks multiple interacting distributed application components by running them in a single JVM and simulating the behavior of the network within the same JVM via stub classes. Unit verification targets a single component of a distributed application and requires that the user write an event generator class that utilizes the API exported by the framework.