CHET: Statically Checking Software Systems

Overview

The behavior of software systems is complex and often problematic. This is especially true when modern systems make use of complex components (in the form of web services, classes, or libraries) that are supposed to be used in a particular way. CHET is a software package that is designed to allow the developer to define the behavior of such components (or actually of any part of a system) and then statically check whether that behavior occurs in a large Java system.

CHET starts with a specification defined as an extended finite state automata over a set of parameterized events. The events are parameterized in that they can define or refer to variables. For example, an allocation event can define a variable corresponding to the object being created and a call event can then refer to the 'this' parameter of the call and assert it has to be the same as the allocated object. The automata are extended in that they include the variables and may have conditions associated with the arcs.

Based on the automata defining what conditions to check, CHET does a full interprocedural flow analysis of the byte codes of the Java system. It is able to handle most of the complexities of Java including native methods, callbacks, threads, and exceptions. The flow analysis is used to identify the potential sources for each of the events and to later simplify checking by identifying unexcutable code or code that is irrelevant to a particular event.

Next CHET finds the conditions to check. This is done by finding all instances of the initial event for each of the specifications being checked. For each such instance, CHET builds an abstract program. This program consists of methods modeled as automata with nodes representing calls, variable sets, return sets, synchronizations, returns, tests, and asynchronous calls. The program is simplified as much as possible for each condition.

Finally, for each resultant program, CHET does a form of model checking to determine if the specification always holds, never holds, or sometimes holds. Special handling is used for threads to make this practical and complete. The checker also generates a report showing a program trace for each reachable final state of the specification automata.

Papers

CHET: A System for Checking Dynamic Specifications, Steven P. Reiss, unpublished, 2004.

Images

The User interface showing a specifcation, the abstract program that is generated for that specification, and, for an piece of the trace that goes with the specification, where in the source and the two automata the trace is.

Software

CHET is available as part of the CLIME system.