Where academic tradition
meets the exciting future

You are here: TUCS > PUBLICATIONS > Publication Search > A Case Study in Formal Develop...

A Case Study in Formal Development of a Fault Tolerant Multi-Robotic System

Inna Pereverzeva, Elena Troubitsyna, Linas Laibinis, A Case Study in Formal Development of a Fault Tolerant Multi-Robotic System. In: Paris Avgeriou (Ed.), Proceedings of the 4th International Workshop on Software Engineering for Resilient Systems (SERENE 2012), Lecture Notes in Computer Science 7527, 16–31, Springer-Verlag Berlin Heidelberg, 2012.

Abstract:

Multi-robotic systems are typical examples of complex multi-agent systems. The robots – autonomic agents – cooperate with each other in order to achieve the system goals. While designing multi-robotic systems, we should ensure that these goals remain achievable despite robot failures, i.e., guarantee system fault tolerance. However, designing the fault tolerance mechanisms for multi-agent systems is a notoriously difficult task. In this paper we describe a case study in formal development of a complex fault tolerant multi-robotic system. The system design relies on cooperative error recovery and dynamic reconfiguration. We demonstrate how to specify and verify essential properties of a fault tolerant multi-robotic system in Event-B and derive a detailed formal system specification by refinement. The main objective of the presented case study is to investigate suitability of a refinement approach for specifying a complex multi-agent system with co-operative error recovery.

BibTeX entry:

@INPROCEEDINGS{inpPeTrLa12d,
  title = {A Case Study in Formal Development of a Fault Tolerant Multi-Robotic System},
  booktitle = {Proceedings of the 4th International Workshop on Software Engineering for Resilient Systems (SERENE 2012)},
  author = {Pereverzeva, Inna and Troubitsyna, Elena and Laibinis, Linas},
  volume = {7527},
  series = {Lecture Notes in Computer Science},
  editor = {Avgeriou, Paris},
  publisher = {Springer-Verlag Berlin Heidelberg},
  pages = {16–31},
  year = {2012},
  keywords = {Event-B, formal modelling, refinement, fault tolerance, multi-robotic system.},
}

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

Publication Forum rating of this publication: level 1

Edit publication