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 . 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.