Formal Development of Critical Multi-agent Systems: A Refinement Approach
Inna Pereverzeva, Elena Troubitsynå, Linas Laibinis · 2012
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.