MAPE-K Interfaces for Formal Modeling of Real-Time Self-Adaptive Multi-Agent Systems

Formal modeling of multi-agent systems is an active area of research. The use of precise and unambiguous notation of formal methods is used to accurately describe and reason about the system under consideration at the design time. Multi-agent systems deployed in dynamic and unpredictable environment needs to have the ability of self-adaptation, making them adaptable to the failures. State of the art encourages the use of MAPE-K feedback loop for the provision of self-adaptation in any system. There is a dire need of formal vocabulary that can be used for the conceptual design of any real-time multi-agent system with self-adaptation. In this paper, we have proposed a set of predefined interfaces for the provision of self-adaptation in real-time multi-agent systems. The interfaces are based on monitor, analyze, plan, and execute phases of the MAPE-K feedback loop. We formally specify our interfaces using timed-communicating object-Z language. The complete framework is elaborated using a trivial case-study of conveyor belt system based on a real-time agent architecture.