A refinement-based approach to developing critical multi-agent systems Online publication date: Tue, 29-Apr-2014
by Inna Pereverzeva; Elena Troubitsyna; Linas Laibinis
International Journal of Critical Computer-Based Systems (IJCCBS), Vol. 4, No. 1, 2013
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.
Existing subscribers:
Go to Inderscience Online Journals to access the Full Text of this article.
If you are not a subscriber and you just want to read the full contents of this article, buy online access here.Complimentary Subscribers, Editors or Members of the Editorial Board of the International Journal of Critical Computer-Based Systems (IJCCBS):
Login with your Inderscience username and password:
Want to subscribe?
A subscription gives you complete access to all articles in the current issue, as well as to all articles in the previous three years (where applicable). See our Orders page to subscribe.
If you still need assistance, please email subs@inderscience.com