Where academic tradition
meets the exciting future

A Refinement-Based Approach to Developing Critical Multi-Agent Systems

Inna Pereverzeva, Elena Troubitsyna, Linas Laibinis, A Refinement-Based Approach to Developing Critical Multi-Agent Systems. International Journal of Critical Computer-Based Systems 4(1), 69–91, 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.

BibTeX entry:

@ARTICLE{jPeTrLa13a,
  title = {A Refinement-Based Approach to Developing Critical Multi-Agent Systems},
  author = {Pereverzeva, Inna and Troubitsyna, Elena and Laibinis, Linas},
  journal = {International Journal of Critical Computer-Based Systems},
  volume = {4},
  number = {1},
  publisher = {Inderscience Enterprises Ltd.},
  pages = {69–91},
  year = {2013},
  keywords = {Event-B, refinement, formal modelling, formal verification, safety, multi-agent system},
}

Belongs to TUCS Research Unit(s): Distributed Systems Laboratory (DS Lab)

Publication Forum rating of this publication: level 1

Edit publication