Refinement-Based Modelling and Verification of, Design Patterns for, Self-adaptive Systems

Abstract

Design patterns are essential for designing complex systems by reusing recurring design principles. Various design patterns were proposed for self-adaptive systems, but their integration into a model-driven design process that, at the same time, provides formal guarantees is still a challenge. This is especially true for self-adaptive design patterns that are generic and abstract enough to provide general solutions that need to be refined prior to their concrete instantiations. In this paper, we present a structured and comprehensible modelling approach for design patterns in the refinement-based process calculus CSP. We formally show crucial properties of them and analyse the refinement-based relationship between their components, which generalises to entire patterns. Based on these analysis results, we are able to provide a first step towards a general, formally well-founded framework providing generic solutions for recurring problems in the management of self-adaptive systems.