Modeling and Analyzing MAPE-K Feedback Loops for Self-Adaptation

The MAPE-K (Monitor-Analyze-Plan-Execute over a shared Knowledge) feedback loop is the most influential reference control model for autonomic and self-adaptive systems. This paper presents a conceptual and methodological framework for formal modeling, validating, and verifying distributed self-adaptive systems. We show how MAPE-K loops for self adaptation can be naturally specified in an abstract stateful language like Abstract State Machines. In particular, we exploit the concept of multi-agent Abstract State Machines to specify decentralized adaptation control by using MAPE computations. We support techniques for validating and verifying adaptation scenarios, and getting feedback of the correctness of the adaptation logic as implemented by the MAPE-K loops. In particular, a verification technique based on meta-properties is proposed to allow discovering unwanted interferences between MAPE-K loops at the early stages of the system design. As a proof-of concepts, we model and analyze a traffic monitoring system.