Affordable Access

deepdyve-link
Publisher Website

Runtime Verification of Timed Properties in Autonomous Robots

Authors
  • Foughali, Mohammed
  • Bensalem, Saddek
  • Combaz, Jacques
  • Ingrand, Félix
Publication Date
Dec 02, 2020
Identifiers
DOI: 10.1109/MEMOCODE51338.2020.9315156
OAI: oai:HAL:hal-03093298v1
Source
HAL-INRIA
Keywords
Language
English
License
Unknown
External links

Abstract

Throughout the last few decades, researchers and practitioners are showing more and more interest in using formal methods in order to predict and prevent software failures in robotic and autonomous systems. However, the applicability of formal methods to such systems is limited due to several factors. For instance, robotic specifications are often non-formal which makes their formalization hard and error prone, and their translation into formal models ad-hoc and non automatic. Furthermore, the complexity and size of robotic applications lead most often to scalability issues with exhaustive techniques such as model checking. In this paper, we investigate the use of runtime verification as an alternative to model checking for the rigorous verification of large robotic systems. To do so, we first develop a sound and automatic translation from the robotic framework GenoM3 to the real-time version of the BIP formal language. Then, we apply the translation to a real-world case study the formal models of which do not scale with model checking, and use the BIP Engine to execute the generated BIP model, verify properties online, and adequately react to their possible violation. The experiments are carried out on a real Robotnik robot and show the efficiency of our approach in verifying timed properties, that is when the amount of time separating events is important.

Report this publication

Statistics

Seen <100 times