Design component contracts: Modeling and analysis of pattern-based composition

Component-based software development focuses on building large software systems by integrating existing software components. In object-oriented design, expert design experience is packaged as design patterns. Software patterns are a new design paradigm used to solve problems that arise when developing software within a particular context. Patterns capture the static and dynamic structure and collaboration among the components in a software design. A key promise of the pattern-based approach is that it may greatly simplify the construction of software systems out of building blocks and thus reuse experience and reduce cost. However, it also introduces significant problems in ensuring the integrity and reliability of these composed systems because of their complex software topologies, interactions, and transactions. There is a need to capture these features as a contract through a formal model that allows us to analyze pattern-based designs. The objective of this thesis is to define a formal framework for ensuring the integrity of the compositions in object-oriented designs by providing mathematically rigorous modeling and analysis techniques for object-oriented systems comprising pattern-based designs as the basic building blocks or design components.; Most existing techniques on modeling software design components are based on informal design notations, such as UML, which lack the support for rigorous analysis. To enable pattern-based software specifications to be analyzed in a mathematically rigorous manner, and thereby provide designers with feedback in advance of implementation, we will pursue the following lines of inquiry: (i) the definition of design component contract that is a formal model of design component based on process calculus and logic programming; (ii) the separation of different aspects (e.g., structure and behavior) of design component contracts such that distinct aspects of the contracts and their compositions can be specified and analyzed both independently and jointly; (iii) the definition of a set of properties that can be used to analyze the design component and its properties so that the properties can be mechanized verified against the contracts; (v) the verification of design components in order to analyze through model checking and Prolog proofs whether composition properties hold; (vi) and a case study applying the systematic approach to specify and verify the composition of design components in the hypermedia domain. This research will enhance the capabilities of formal system modeling and analysis by providing a rigorous basis for high-assurance integration of diverse pattern-based components.