A framework for interactive verification of architectural design patterns in isabelle/hol

Abstract

Architectural design patterns capture architectural design experience and are an important tool in software engineering to support the conceptualization and analysis of architectures. They constrain different aspects of an architecture and usually guarantee some corresponding properties for architectures implementing them. Verifying such patterns requires proving that the constraints imposed by the pattern indeed lead to architectures which satisfy the corresponding guarantee. Due to the abstract nature of patterns, verification is often done by means of interactive theorem proving and requires detailed knowledge about the underlying model, limiting its application to experts of this model. Moreover, proving properties for different patterns usually involves repetitive proof steps, leading to proofs which are difficult to maintain. To address these problems, we developed a framework that supports the interactive verification of architectural design patterns in Isabelle/HOL. The framework implements a model for dynamic architectures as well as a corresponding calculus in terms of two Isabelle/HOL theories and consists of roughly 3500 lines of Isabelle/HOL proof script. To evaluate our framework, we applied it for the verification of four different architectural design patterns and compared the overall amount of proof code to the code contributed by the framework. Our results suggest that the framework has the potential to significantly reduce the amount of proof code required for the verification of patterns and thus to address the problems mentioned above.