The project objective is to create an environment for formally specifying, composing, and refining software systems at the architecture level. These capabilities will extend our formal design infrastructure, Quiver, whose development is ongoing. Integration of large systems is difficult and expensive. A one-time solution to integration, such as glue code, is not sufficient: components evolve, invariably leading to incompatibilities and new interface requirements. We propose a comprehensive solution to this problem via the use of formally defined interfaces that capture enough semantics to allow correct integration of components and software architectures, formally represented as coherent collections of components that allow system refinement and evolution. Our approach introduces formality incrementally into the integration process: only parts relevant to specific integration issues need be formalized. In other words, system measures such as evolvability will be proportional to the degree of formalization. This flexible incremental approach to the integration problem provides a valuable opportunity to demonstrate the efficacy of formal methods in large-scale software systems. The innovative aspects of our technology lies in the creative combination of concepts from several mathematical disciplines; the realization of the combined theoretical framework using leading-edge, mainstream technologies; and the visual interface to the semantic design structures
