Title: A refinement-based approach to developing critical multi-agent systems

Authors: Inna Pereverzeva; Elena Troubitsyna; Linas Laibinis

Addresses: Turku Centre for Computer Science, Åbo Akademi University, Joukahaisenkatu 3-5, 20520 Turku, Finland ' Åbo Akademi University, Joukahaisenkatu 3-5A, 20520 Turku, Finland ' Åbo Akademi University, Joukahaisenkatu 3-5A, 20520 Turku, Finland

Abstract: Multi-agent systems are increasingly used in critical applications. To ensure dependability of multi-agent systems, we need powerful development techniques that would allow us to master complexity inherent to such kind of systems and formally verify correctness and safety of collaborative agent activities. In this paper, we present a rigorous approach to the development and verification of critical multi-agent system in Event-B. We demonstrate how to formally specify complex agent interactions and verify their correctness and safety. We argue that the refinement approach facilitates structuring complex requirements and formal reasoning about system-level properties. We illustrate our approach by a case study: formal development of a hospital multi-agent system.

Keywords: Event-B; refinement; formal modelling; formal verification; formal methods; safety; multi-agent systems; hospital MAS; critical systems; agent-based systems; collaborative agents; patient monitoring; healthcare technology; patient record updating; patient records; medical records; data security; e-healthcare; electronic healthcare.

DOI: 10.1504/IJCCBS.2013.053743

International Journal of Critical Computer-Based Systems, 2013 Vol.4 No.1, pp.69 - 91

Published online: 29 Apr 2014 *

Full-text access for editors Full-text access for subscribers Purchase this article Comment on this article