Design-by-contract for software architectures

We propose a design by contract (DbC) approach to specify and maintain architectural level properties of software. Such properties are typically relevant in the design phase of the development cycle but may also impact the execution of systems. We give a formal framework for specifying software architectures (and their refi nements) together with contracts that architectural con figurations abide by. In our framework, we can specify that if an architecture guarantees a given pre- condition and a refi nement rule satisfi es a given contract, then the refi ned architecture will enjoy a given post-condition. Methodologically, we take Architectural Design Rewriting (ADR) as our architectural description language. ADR is a rule-based formal framework for modelling (the evolution of) software architectures. We equip the recon figuration rules of an ADR architecture with pre- and post-conditions expressed in a simple logic; a pre-condition constrains the applicability of a rule while a post-condition specifi es the properties expected of the resulting graphs. We give an algorithm to compute the weakest precondition out of a rule and its post-condition. Furthermore, we propose a monitoring mechanism for recording the evolution of systems after certain computations, maintaining the history in a tree-like structure. The hierarchical nature of ADR allows us to take full advantage of the tree-like structure of the monitoring mechanism. We exploit this mechanism to formally defi ne new rewriting mechanisms for ADR reconfi guration rules. Also, by monitoring the evolution we propose a way of identifying which part of a system has been a ffected when unexpected run-time behaviours emerge. Moreover, we propose a methodology that allows us to select which rules can be applied at the architectural level to reconfigure a system so to regain its architectural style when it becomes compromised by unexpected run-time recon figurations.