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

Formal Development and Quantitative Assessment of a Resilient Multi-Robotic System

Anton Tarasyuk, Inna Pereverzeva, Elena Troubitsyna, Linas Laibinis, Formal Development and Quantitative Assessment of a Resilient Multi-Robotic System. In: Anatoliy Gorbenko, Alexander Romanovsky, Vyacheslav Kharchenko (Eds.), Proceedings of the 5th International Workshop on Software Engineering for Resilient Systems (SERENE 2013), Lecture Notes in Computer Science 8166, 109–124, Springer-Verlag Berlin Heidelberg, 2013.

Abstract:

Ensuring resilience of multi-robotic systems is a notoriously difficult task. Decentralised architectures and asynchronous communication require powerful modelling techniques to demonstrate system resilience. In this paper, resilience of a multi-robotic system is defined as the ability to achieve goals despite robot failures. We demonstrate how to rigorously specify and verify essential properties of resilience mechanisms of multi-robotic systems by refinement in Event-B. To assess the desired
resilience characteristics, we augment our formal models with statistical data and rely on probabilistic verification. The automated support provided by the PRISM model checker allows us to calculate the probability of goal reachability in the presence of robot failures and compare different reconfiguration strategies for selected architectures. We demonstrate our approach by a case study – development and assessment of a cleaning multi-robotic system.

BibTeX entry:

@INPROCEEDINGS{inpTaPeTrLa13a,
  title = {Formal Development and Quantitative Assessment of a Resilient Multi-Robotic System},
  booktitle = {Proceedings of the 5th International Workshop on Software Engineering for Resilient Systems (SERENE 2013)},
  author = {Tarasyuk, Anton and Pereverzeva, Inna and Troubitsyna, Elena and Laibinis, Linas},
  volume = {8166},
  series = {Lecture Notes in Computer Science},
  editor = {Gorbenko, Anatoliy and Romanovsky, Alexander and Kharchenko, Vyacheslav},
  publisher = {Springer-Verlag Berlin Heidelberg},
  pages = {109–124},
  year = {2013},
  keywords = {Formal modelling, resilience, Event-B, refinement, probabilistic model checking, multi-robotic system},
}

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

Publication Forum rating of this publication: level 1

Edit publication