Engineering and Employing Reusable Software Components for Modular Verification

The aim of this paper is to illustrate the central role of reusable software components in developing high assurance software systems and a practical framework and environment for building such systems. The paper presents in detail elements of an actual implementation of a component- based system wherein all components are engineered for reuse and are equipped with interface contracts formalized via mathematical models so that they are amenable to automated verification. The components in the system themselves are built reusing other components, and for scalability, can be verified in a modular fashion one component at a time, using only the interface contracts of reused components. While building such components is necessarily expensive, reuse has the power to amortize the costs. Specification, research, development, verification, and reuse of components in this paper have been performed in the context of an experimental, desktop-based IDE we have built.