Logo
ScienceStack
Table of Contents
Fetching ...
Sign In

ROSMonitoring 2.0: Extending ROS Runtime Verification to Services and Ordered Topics

Maryam Ghaffari Saadat, Angelo Ferrando, Louise A. Dennis, Michael Fisher

TL;DR

ROSMonitoring 2.0 is introduced, an extension of ROSMonitoring designed to facilitate the monitoring of both topics and services while considering the order in which messages are published and received, offering improved real-time support, security, scalability, and interoperability.

Abstract

Formal verification of robotic applications presents challenges due to their hybrid nature and distributed architecture. This paper introduces ROSMonitoring 2.0, an extension of ROSMonitoring designed to facilitate the monitoring of both topics and services while considering the order in which messages are published and received. The framework has been enhanced to support these novel features for ROS1 -- and partially ROS2 environments -- offering improved real-time support, security, scalability, and interoperability. We discuss the modifications made to accommodate these advancements and present results obtained from a case study involving the runtime monitoring of specific components of a fire-fighting Uncrewed Aerial Vehicle (UAV).

ROSMonitoring 2.0: Extending ROS Runtime Verification to Services and Ordered Topics

TL;DR

ROSMonitoring 2.0 is introduced, an extension of ROSMonitoring designed to facilitate the monitoring of both topics and services while considering the order in which messages are published and received, offering improved real-time support, security, scalability, and interoperability.

Abstract

Formal verification of robotic applications presents challenges due to their hybrid nature and distributed architecture. This paper introduces ROSMonitoring 2.0, an extension of ROSMonitoring designed to facilitate the monitoring of both topics and services while considering the order in which messages are published and received. The framework has been enhanced to support these novel features for ROS1 -- and partially ROS2 environments -- offering improved real-time support, security, scalability, and interoperability. We discuss the modifications made to accommodate these advancements and present results obtained from a case study involving the runtime monitoring of specific components of a fire-fighting Uncrewed Aerial Vehicle (UAV).

Paper Structure

This paper contains 14 sections, 2 theorems, 7 figures, 4 tables.

Table of Contents

  1. Introduction
  2. Preliminaries
  3. Runtime Verification
  4. ROSMonitoring
  5. Instrumentation
  6. Oracle
  7. ROS monitor
  8. Motivating example
  9. ROSMonitoring 2.0
  10. Service extension
  11. Ordered topics extension
  12. Experimental evaluation
  13. Related Work
  14. Conclusions and Future Work

Key Result

Lemma 1

In Algorithm alg:ordered-msgs, messages in each buffer maintain the order of publication timestamps.

Figures (7)

  • Figure 1: High-level overview of ROSMonitoring DBLP:conf/taros/FerrandoC0AFM20.
  • Figure 2: Motivating example with three components: Battery, Battery Supervisor, and LED Panel. Battery publishes on topic $\mathit{/battery\_percentage}$; Battery Supervisor subscribes to $\mathit{/battery\_percentage}$, publishes on topic $\mathit{/battery\_status}$, and invokes service $\mathit{/SetLED}$; LED Panel publishes on topic $\mathit{/LED\_Panel}$ and responds to $\mathit{/SetLED}$ service requests.
  • Figure 3: Service verification in ROSMonitoring 2.0 when filtering is enabled.
  • Figure 4: Case study with ROS Monitor and additional topics $\mathit{/input\_accepted}$, $\mathit{/status\_accepted}$, $\mathit{/status\_change}$, $\mathit{/verdict}$ and service $\mathit{/SetLED\_mon}$.
  • Figure 5: Mean and standard deviation of time (nanoseconds) taken for monitor with ordering to buffer and release messages on $\mathit{/battery\_percentage}$ (top), $\mathit{/input\_accepted}$ (middle), ans $\mathit{/battery\_status}$ (bottom) topics since publication. Data shown for 10 runs.
  • ...and 2 more figures

Theorems & Definitions (4)

  • Lemma 1
  • proof
  • Theorem 1
  • proof