Formal Development of Critical Multi-agent Systems: A Refinement Approach

Multi-agent systems (MAS) are increasingly used in critical applications. To ensure dependability of MAS, we need powerful development techniques that would allow us to master complexity inherent to MAS and formally verify correctness and safety of collaborative agent activities. In this paper we present a development of hospital MAS by refinement in Event-B. We demonstrate that Event-B allows the developers to rigorously specify complex agent interactions and verify their correctness and safety.