A Correct by Construction Approach For Modeling and Formalizing Self-adaptive Systems

Self-adaptive systems adapt their own behavior autonomously in order to control the satisfaction of their requirements under changing environmental conditions. MAPE (Monitor, Analyze, Plan and Execute) control loops have been used as important models for realizing self-adaptation. Adaptive systems are generally more difficult to design, specify and verify due to their high complexity. In this paper, we propose a formal refinement approach that aims first to model self-adaptive systems based on MAPE control loop. Second, our approach aims to formally specify self-adaptive systems at a high level of abstraction using the Event-B method providing correct by construction software. This formal specification provides a way to verify correctness of self-adaptive systems regarding a number of criteria. We provide a software tool (as an Eclipse plug-in) that supports designers in their architectural choices by defining a set of patterns describing the different ways of organizing MAPE loops, such as Master/Slave, coordinated control and hierarchical control. We illustrate our approach within a marine monitoring environment case study for validation purpose.