Composing pattern-based components and verifying correctness

Designing large software systems out of reusable components has become increasingly popular. Although liberal composition of reusable components saves time and expense, many experiments indicate that people will pay for this (liberal composition) sooner or later, sometimes paying even a higher price than the savings obtained from reusing components. Thus, we advocate that more rigorous analysis methods to check the correctness of component composition would allow combination problems to be detected early in the development process so that people can save the considerable effort of fixing errors downstream. In this paper we describe a rigorous method for component composition that can be used to solve combination and integration problems at the (architectural) design phase of the software development lifecycle. In addition, we introduce the notion of composition pattern in order to promote the reuse of composition solutions to solve routine component composition problems. Once a composition pattern is proven correct, its instances can be used in a particular application without further proof. In this way, our proposed method involves reusing compositions as well as reusing components. We illustrate our approach through an example related to the composition of design patterns as design components. Structural and behavioral correctness proofs about the composition of design patterns are provided. Case studies are also presented to show the applications of the composition patterns.