Large software systems are usually made up of a number of components, not all of which are produced by a single development team. Making sure that separately designed components can cooperate is a major challenge in building a large system, and the difficulty is compounded when components change over time. When can an updated version of a software component, like a new version of a networking library, be added to a system without disrupting its correct operation? Programming languages enforce syntactic interface specifications like the argument types of methods, but some of the hardest-to-avoid problems come from semantic changes in the implied specification of a component. While specifying and proving the complete behavior of each component would eliminate mismatches in theory, complete specification is impractical for large-scale systems.
We use an automated tool to infer likely invariants over a component's execution, based on observing its behavior at runtime. Besides unit-testing a component in isolation, we can also consider its behavior in a complete, functioning system. These two conjectured specifications will usually differ. On one hand, a particular application may exercise only a subset of a component's capabilities. Conversely, however, applications may also depend on facets of a component's behavior that its designers did not intend to commit to. To more accurately predict whether or not a component upgrade will be disruptive, we can compare the behavior of the component tested on its own, both before and after an upgrade, to the behavior depended upon by the rest of the system. Because this semantic information is more comprehensive than the component's syntactic interface, our hypothesis is that we can use it to more accurately warn when a component upgrade would be ill-advised.
As part of this work, we have developed a Daikon front-end to instrument programs written in Perl. More information about dfepl can be found in the Daikon manual. The tool that performs the logical comparisons between operations abstractions for a component is also included in the Daikon distribution, and documented elsewhere in the Daikon manual.
I presented a version of this work to the 9th New England Programming Languages and Systems Symposium, abstract here.
I presented a version of this work to the MIT CSAIL Programming Systems Graduate Zeminar in August of 2003. A version of the slides for this presentation are available in one-slide-per-page gzipped PostScript, six-slides-per-page gzipped PostScript, one-slide-per-page PDF, or six-slides-per-page PDF.
An early paper describing this work appears in the proceedings of the 10th European Software Engineering Conference and the 11th ACM SIGSOFT Symposium on the Foundations of Software Engineering (ESEC/FSE 2003). Some more recent advances are included in the proceedings of the 18th annual European Conference on Object-Oriented Programming (ECOOP 2004). For abstracts and downloadable versions of these papers, see my PAG publications list.
Some additional implementation details are mentioned in the revision of my Master's thesis as a MIT Lab for Computer Science technical report 941. This may be downloaded in gzipped PostScript or PDF formats.
More recently, I presented a version of this work to the workshop on the Specification and Verification of Component-Based Systems (SAVCBS) at FSE 2004. A version of the slides for this presentation are available in one-slide-per-page gzipped PostScript, six-slides-per-page gzipped PostScript, one-slide-per-page PDF, or six-slides-per-page PDF.