Checking Software Component Interfaces

We focus on component based software verification and early (design time) error detection based on a behavioral type system defining temporal properties of software component interfaces.

Interface theories are a very general formalism for expressing design time assumptions made by a component about the behavior of the environment it is to be deployed in, and have been used in a wide variety of systems, concurrent, single-threaded, asynchronous, synchronous, recursive, etc. [1-5], and used to express many kinds of environment assumptions.

We focus on interfaces for software systems involving recursive programs and expressing method invocation protocols [4]. Checking compatibility of two systems in this context involves solving a reachability game with two players on the configuration graph of a pushdown automaton.

There are several interesting applications of this treatment. It is possible to detect incompatiblities between components locally. For example, we have found method call order protocol violation errors in the TinyOS system, an operating system for ad-hoc networked sensors developed by systems researchers at UC Berkeley.

We have implemented CHIC, a checker for checking compatibility of a variety of interface formalisms. CHIC is available as a plug-in for the popular Java IDE, JBuilder.

[1]

L. de Alfaro and T. A. Henzinger, "Interface Automata," Proc. Symp. Foundations of Software Engineering, Vienna, Austria, September 2001.

[2]

L. de Alfaro and T. A. Henzinger, "Interface Theories for Component-based Design," Proc. Int. Workshop on Embedded Software, Tahoe City, CA, October 2001.

[3]

A. Chakrabarti, L. de Alfaro, T. A. Henzinger, and F. Y. C. Mang, "Synchronous and Bidirectional Component Interfaces," Proc. Int. Conf. Computer-Aided Verification, Copenhagen, Denmark, July 2002.

[4]

A. Chakrabarti, L. de Alfaro, T. A. Henzinger, M. Jurdzinski, and F. Y. C. Mang, "Interface Compatibility Checking for Software Modules," Proc. Int. Conf. Computer-Aided Verification, Copenhagen, Denmark, July 2002.

[5]

L. de Alfaro, T. A. Henzinger, and M. Stoelinga, "Timed Interfaces," Proc. Int. Workshop on Embedded Software, Grenoble, France, October 2002.