Affordable Access

deepdyve-link
Publisher Website

Bridging the Gap between Formal Verification and Schedulability Analysis: The Case of Robotics

Authors
  • Foughali, Mohammed
  • Hladik, Pierre-Emmanuel
Publication Date
Dec 01, 2020
Identifiers
DOI: 10.1016/j.sysarc.2020.101817
OAI: oai:HAL:hal-02864928v2
Source
HAL-Descartes
Keywords
Language
English
License
Unknown
External links

Abstract

The challenges of deploying robots and autonomous vehicles call for further efforts to bridge the gap between the robotics, the real-time systems and the formal methods communities. Indeed, with robots being more and more involved in costly missions and contact with humans, a rigorous formal verification of their behavior in the presence of various real-time constraints is crucial. In order to increase our trust in its results, such verification should be carried out on models that are the closest possible to reality, and thus take into account hardware and OS specificities such as the number of cores provided by the robotic platform and the scheduling policy. In this paper, we propose a novel binary-search-inspired technique that allows to extend timed automata models of robotic specifications with dynamic-priority schedulers. Given a number of cores, the extended models can then be checked against various real-time and behav-ioral properties, including schedulability, within the same model checking framework. Our technique is implemented in an automatic translation from a robotic framework to UPPAAL, and evaluated on a real robotic case study, where it shows a significant gain in scalability as opposed to the counting technique used in the literature.

Report this publication

Statistics

Seen <100 times