Purpose:

The software industry is increasingly concerned with the reusability of software components, not just as a means of increasing productivity within individual organizations but also with an eye towards reusable software components as objects of commerce. Libraries of relatively independent components --e.g. mathematical software for engineering-- have long been common, but have not had major commercial impact. Contemporary component software libraries provide components that fit together in some framework of concepts and standardized interfaces. A significant limiting factor on commerce in software component libraries is reliability: vendor often provide very imprecise and incomplete specifications, and offer little guarantee that their components meet those specifications. The power and flexibility of object-oriented languages which makes components practical also makes it difficult to validate that they meet their specifications. This situation becomes increasingly untenable as components are used in mission -and life- critical applications.

Approach:

Our research will demonstrate that significant improvement in quality increases the profitability of component software. This will involve the development of a small verified library, perhaps for computational geometry. It will also involve the development of supporting tools.

Status:

Modular Verification of Extensible Software Components

My current research focus is on source-level verification of software components, especially object classes, using both fully automated techniques (model checking) and partially automated ones (proof, abstraction, and approximation for infinite-state systems).

1. In one project I am working with an industrial collaborator on model checking for inter-procedural analysis of safety and security properties using approximation techniques and building on recent advances in checking pushdown processes.

2. With a colleague at Stevens I am developing techniques for modular analysis of safety and liveness properties of mobile code for web-based services. We are especially interested in dynamic verification based on precomputed analyses (as in proof-carrying code).

3. Another of my projects has developed a verification calculus for behavioral subclassing and specification of object-oriented frameworks. On this basis, my collaborators are developing tools for refactoring class structure and for program transformation in compilation.

4. Class-level component libraries have not fulfilled their promise for productivity gains through reuse, much less for commercially viable commerce in components. One of my projects is concerned with class transformers as extensible components.

Related Publications:

A weakest precondition semantics for refinement in an object-oriented language, David Naumann and Ana Cavalcanti.
Formal Methods '99, Jeannette M. Wing, Jim Woodcock, and Jim Davies, eds., Springer LNCS 1709. There is also a Stevens Tech Report 9903.

A Weakest Precondition Semantics for an Object-oriented Language of Refinement, David Naumann and Ana Cavalcanti.
IEEE Transactions on Software Engineering 26(8) August 2000.

Calculating Sharp Adaptation Rules, David Naumann
To appear in Information Processing Letters (2000).

Class refinement for sequential java, David Naumann and Ana Cavalcanti.
In ECOOP 2001 Workshop on Formal Techniques for Java Programs, S. Eisenbach, G.T. Leavens, P. Mueller, A. Poetzsch-Heffter, E. Poll, eds.