Introduction

Large software systems are usually made up of a number of components, not all produced by a single development team. Ensuring 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. System integrators would often like to know whether an updated version of a software component can be added to a system without disrupting its correct operation.

We have developed a new technique to assess whether replacing one or more components of a software system by purportedly compatible components will change the behavior of the system. The technique operates prior to integrating the new components into the system, permitting quicker and cheaper identification of problems. It takes into account the system's use of the components, because an upgrade may be desirable in one context but undesirable in another. No formal specifications are required, permitting detection of problems due to errors in the components or errors in the system. Both external and internal behaviors can be compared, enabling detection of problems that are not immediately reflected in the system's output.

Technique

The two key techniques that underly our method are describing observed behavior and comparing those behaviors via logical implication. We characterize behavior via dynamic detection of likely program invariants, which generalizes over program executions to produce an operational abstraction: a set of formal mathematical properties describing the observed behavior. An operational abstraction is syntactically identical to a formal specification, describing program behavior via formulas over program variables, but it describes actual program behavior and can be generated automatically, whereas a specification describes desired program behavior and is provided by a human before the code is written. Operational abstractions are more useful for our purposes than specifications, because we want to find incompatibilities induced by the actual behavior of the software.

Because operational abstractions are simply collections of statements in a formal language, they can be mechanically compared to determine if one abstraction is logically implied by another. If our system, using an automatic theorem prover, can verify that the abstraction describing a component's desired behavior is a logical consequence of the abstraction of its observed behavior during testing, we have evidence that the component will indeed function correctly.

Progress

We have formulated a general model for the semantics of a multi-component system, based on a division into modules with certain behaviors and certain expectations of the behavior of other modules. This model encompasses a variety of component interactions, including components with state, access to shared variables, callbacks, and upgrades that require the simultaneous replacement of multiple components. From this model, we use an algorithm to construct logical relations which, if they hold over the operational abstractions of a set of components, indicate that each component's expectations will be satisfied when the system executes. These relations are then checked using the Simplify automatic theorem prover. We have supplemented the basic technique with several enhancements that make it more effective in practical applications: these deal with nonlocal data and nondeterministic behavior, and allow the technique to differentiate between preexisting innocuous incompatibilities from more dangerous new ones.

We have evaluated an implementation of the technique with case studies applying it to real-world components: Perl modules from the Comprehensive Perl Archive Network (CPAN) [1], and the main Linux system library, as used by 48 applications [2]. In these case studies, the technique verifies the safety of some upgrades, while discovering incompatibilities in other upgrades that cause applications to malfunction. Our technique's comparisons can be performed efficiently, and its rate of false positive warnings is low (Figure 1).

Figure 1. Reported incompatibilities between Linux C library versions 2.1.3 and 2.3.2 for 48 subject programs. Yellow bars represent incompatibilities that we have verified by hand. Green bars represent warnings that are probably false positives.

In ongoing research [3], we are focusing on giving a precise description of the multi-component upgrade condition in the context of a simplified formal model. The model idealizes the operational abstractions used by the technique to abstractions that soundly approximate the behavior of the components they describe. A soundness result for the formalization (which we have so far achieved for the case of a two-component upgrade) corresponds to a relative soundness of the real system, which restricts the source of unsoundness to the finiteness of the testing used in constructing the abstractions. Work on the formalization has also motivated refinements and led to a better understanding of the technique as implemented, including trade-offs between accuracy and performance.

Future

We would like to examine how our technique performs in different software architectures, and whether it can be extended to interactions between processes in a distributed context, or between separate applications sharing system resources. Based on insights gained while formalizing the technique, we would like to increase the technique's context sensitivity when needed, without performing unnecessary duplication when it would be redundant. Finally, we would like to explore whether the logical comparison between abstractions can be performed better by a specialized tool operating as a pre-processor for or instead of a general theorem prover.

Research Support

This research is supported in part by the National Science Foundation (grants CCR-0133580 and CCR-0234651), by DARPA contract FA8750-04-2-0254, by the Oxygen project, by gifts from NTT and the Edison Design Group, by an MIT Presidential (Akamai) Graduate Fellowship, and by a National Defense Science and Engineering Graduate Fellowship.

References:

[1] Stephen McCamant and Michael D. Ernst. Predicting problems caused by component upgrades. In Proceedings of the 10th European Software Engineering Conference and the 11th ACM SIGSOFT Symposium on the Foundations of Software Engineering, pp. 287-296, Helsinki, Finland, September 2003.

[2] Stephen McCamant and Michael D. Ernst. Early identification of incompatibilities in multi-component upgrades. In ECOOP 2004 -- Object-Oriented Programming, 18th European Conference, pp. 440-464, Olso, Norway, June 2004.

[3] Stephen McCamant and Michael D. Ernst. Formalizing lightweight verification of software component composition. In Specification and Verification of Component-Based Systems Workshop pp. 47-54, Newport Beach, California, USA, October 2004.