• TUCS Publication Series
• How to Publish in TUCS Series
• Publication Search
• Publication Graph
• Publication Input
• Publication Input Guide
• JuFo Browser

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

Inna Pereverzeva, Elena Troubitsyna, Linas Laibinis, A Case Study in a Formal Development of a Fault Tolerant Multi-Robotic System. TUCS Technical Reports 1052, Turku Centre for Computer Science, 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.

Files:

Full publication in PDF-format

BibTeX entry:

@TECHREPORT{tPeTrLa12b,
  title = {A Case Study in a Formal Development of a Fault Tolerant Multi-Robotic System},
  author = {Pereverzeva, Inna and Troubitsyna, Elena and Laibinis, Linas},
  number = {1052},
  series = {TUCS Technical Reports},
  publisher = {Turku Centre for Computer Science},
  year = {2012},
  keywords = {Event-B, formal modelling, refinement, fault tolerance, multi-robotic system},
  ISBN = {978-952-12-2766-0},
}

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

Edit publication