Automated component retrieval and adaptation using formal specifications

This work describes the use of formal specifications to assist and automate a system design process based on reusable components and architectures. Specifically, we focus on automated support for two reuse-related component-based design activities: (1) identification and retrieval of library components pertinent to the problem at hand, and (2) identification and application of structures for architectures) available for adapting these components.;Formally verifying that a logical relationship holds between two specifications (a.k.a. specification matching (134)) to determine component reusability can be carried out using automated theorem proving. However, attempting specification matching over a large library of components is not a practical retrieval mechanism. To make specification matching efficient, it must be restricted to a small subset of the database. We have developed a heuristic for determining this subset of components based on the semantics provided by formal component interface specifications. A feature-based indexing scheme is used to classify components and allow efficient retrieval. A set of domain dependent classification rules state logical conditions defining when a component should be assigned specific features. If one of these conditions can be inferred from the component specification then the component is assigned the appropriate feature. We provide a formal argument that this method of classification ie appropriate for determining component reusability. We empirically evaluate the retrieval performance of an implementation of this mechanism over a library of 63 list manipulation components. The results indicate that the method performs as well as other specification-based retrieval systems, but with a faster response time.;In most cases, component retrieval will not locate a component that completely satisfies a problem specification; solving a problem will require a component to be adapted or multiple components to be combined. We propose to use a formal model of software architecture, architecture theories, to automate component adaptation and composition. An architecture theory constrains the behavior of a system in terms of the behavior of its subcomponents via a collection of axioms. This relationship is specified declaratively, abstracting away implementation and focusing on the relationship between the system and component specifications. We show that architecture theories can be used to adapt and combine retrieved components to satisfy a problem specification. We develop several methods for controlling the selection of architectures during adaptation based on the results of component retrieval. The adaptation system is evaluated by constructing and adapting variations of the KWIC problem from the Model Problems in Software Architecture Archive and the JPEG compression algorithm.