Class libraries and software components are supposed to make building complex applications from "parts" easier, make a market for pre-packaged code...

...but in practice, programming with components is hard, due to inadequate documentation, lack of source code, and increased API complexity (to allow for customization)

Programmers often resort to iterative trial-and-error methods to get components to work in their application

Allow the component designer to specify component conformance constraints in a natural (yet still formal) way

Provide automated certification tools to determine whether the client satisfies the component's conformance constraints

Initial focus is on Java^TM libraries and JavaBeans^TM

Component behavior in Canvas is specified in a Java-flavored imperative language called Easl. Easl retains much of Java's control flow and declarative machinery, but restricts datatypes to be object references, collections of objects, and primitive types over finite domains (e.g., booleans and enumerations).  Easl also adds special requires and ensures statements that represent constraints and guarantees, respectively, on component state at the point where the statements appear.  Finally, Easl includes a spawn statement for creating concurrent threads, and a waituntil statement to denote synchronization conditions.

We are currently focusing on analysis techniques based on abstract interpretation; the TVLA system is used as test best for analysis techniques and algorithms.

For certain classes of conformance constraint specification for which a straightforward analysis algorithm would have exponential time complexity, we can systematically derive efficient polynomial time analyses.

We currently have an experimental analysis tool for analyzing Java programs.  The tool is based on the  SOOT (McGill) Java bytecode front end.  Given an analysis specification, the tool generates TVLA input that combines the analysis specification with an abstract representation of the Java bytecodes.

The tool has been used to analyze a number of small to medium Java programs, and has discovered several latent bugs.

John Field (IBM Watson)
G. Ramalingam (IBM Watson)
Mooly Sagiv (Tel Aviv University)
Alex Warshavsky (Tel Aviv University)

A presentation describing some of our techniques for deriving efficient analyses and initial results.

An IBM Technical Report describing our techniques; this paper focuses on applications of our technique to analysis of the Concurrent Modification Exception of Java^TM 2 collections.
 

Last modified 29 October 2001. Contact: jfield@watson.ibm.com