Abstract
Multi-agent systems constitute a wide class of decentralised systems. Their functions are usually carried out by collaborative activities of agents. To ensure resilience of multi-agent systems, we should endow them with a capability to dynamically reconfigure. Usually, as a result of reconfiguration, the existing relationships between agents are changed and new collaborations are established. This is a complex and error-prone process, which can be facilitated by the use of formal reasoning and automated verification. In this paper, we propose a generic resilience-explicit formalisation of the main concepts of multi-agent systems. Based on it, we introduce corresponding specification and refinement patterns in Event-B. Our patterns facilitate modelling behaviour of resilient multi-agent systems in a rigorous systematic way and verification of their properties. We demonstrate the application of the proposed approach by a case study—a smart warehouse system.
Original language | English |
---|---|
Journal | Computing |
DOIs | |
Publication status | Published - 2020 |
MoE publication type | A1 Journal article-refereed |