Logo
ScienceStack
Table of Contents
Fetching ...
Sign In

RTAMT -- Runtime Robustness Monitors with Application to CPS and Robotics

Tomoya Yamaguchi, Bardh Hoxha, Dejan Nickovic

TL;DR

The paper tackles scalable runtime verification for CPS and robotics by introducing RTAMT, a tool that computes real-valued robustness of STL specifications at runtime. It presents a modular architecture with a Python front-end and optional C++ back-end, supporting offline and online monitoring in both discrete-time and dense-time interpretations, including bfSTL, pSTL, and IA-STL, with pastification to enable online monitoring. Key contributions include the architectural design, ROS and MATLAB/Simulink integrations, an IA-STL extension with relative robustness and input vacuity, and demonstrations on HSR (ROS) and AECS (Simulink). Results show real-time performance (e.g., online monitoring around 0.5 ms per sample in Python and faster in C++) and practical utility for runtime fault localization and V&V in CPS, motivating further extensions to distributed monitoring and additional specification languages.

Abstract

In this paper, we present Real-Time Analog Monitoring Tool (RTAMT), a tool for quantitative monitoring of Signal Temporal Logic (STL) specifications. The library implements a flexible architecture that supports: (1) various environments connected by an Application Programming Interface (API) in Python, (2) various flavors of temporal logic specification and robustness notion such as STL, including an interface-aware variant that distinguishes between input and output variables, and (3) discrete-time and dense-time interpretation of STL with generation of online and offline monitors. We specifically focus on robotics and Cyber-Physical Systems (CPSs) applications, showing how to integrate RTAMT with (1) the Robot Operating System (ROS) and (2) MATLAB/Simulink environments. We evaluate the tool by demonstrating several use scenarios involving service robotic and avionic applications.

RTAMT -- Runtime Robustness Monitors with Application to CPS and Robotics

TL;DR

The paper tackles scalable runtime verification for CPS and robotics by introducing RTAMT, a tool that computes real-valued robustness of STL specifications at runtime. It presents a modular architecture with a Python front-end and optional C++ back-end, supporting offline and online monitoring in both discrete-time and dense-time interpretations, including bfSTL, pSTL, and IA-STL, with pastification to enable online monitoring. Key contributions include the architectural design, ROS and MATLAB/Simulink integrations, an IA-STL extension with relative robustness and input vacuity, and demonstrations on HSR (ROS) and AECS (Simulink). Results show real-time performance (e.g., online monitoring around 0.5 ms per sample in Python and faster in C++) and practical utility for runtime fault localization and V&V in CPS, motivating further extensions to distributed monitoring and additional specification languages.

Abstract

In this paper, we present Real-Time Analog Monitoring Tool (RTAMT), a tool for quantitative monitoring of Signal Temporal Logic (STL) specifications. The library implements a flexible architecture that supports: (1) various environments connected by an Application Programming Interface (API) in Python, (2) various flavors of temporal logic specification and robustness notion such as STL, including an interface-aware variant that distinguishes between input and output variables, and (3) discrete-time and dense-time interpretation of STL with generation of online and offline monitors. We specifically focus on robotics and Cyber-Physical Systems (CPSs) applications, showing how to integrate RTAMT with (1) the Robot Operating System (ROS) and (2) MATLAB/Simulink environments. We evaluate the tool by demonstrating several use scenarios involving service robotic and avionic applications.

Paper Structure

This paper contains 23 sections, 14 equations, 26 figures, 1 table.

Table of Contents

  1. Introduction
  2. Monitoring Temporal Logic Specifications
  3. Signal Temporal Logic
  4. Pastification from bfSTL to pSTL
  5. Interface-Aware STL
  6. Architecture
  7. Syntax Layer
  8. Semantics Layer
  9. Integration of RTAMT to ROS
  10. Integration of RTAMT to MATLAB/Simulink
  11. Application Programming Interface
  12. Evaluating STL in Offline
  13. Evaluating STL in Online
  14. Evaluating STL on ROS
  15. Textual Specifications for ROS
  16. ...and 8 more sections

Figures (26)

  • Figure 1: Satisfied
  • Figure 2: Violated
  • Figure 4: $\rho( \mathbf{G}\,{[a,b]}\,\varphi, w, t) = \inf_{t' \in [t+a,t+b)} \rho(\varphi, w, t')$
  • Figure 5: $\rho( \mathbf{H}\,_{[a,b]}\,\varphi, w, t) = \inf_{t' \in (t-a,t-b]} \rho(\varphi, w, t')$
  • Figure 7:
  • ...and 21 more figures

Theorems & Definitions (6)

  • Definition 1: Syntax of STL
  • Definition 2: Quantitative Semantics of STL
  • Definition 3: Temporal Depth
  • Definition 4: Pastification Operation
  • Example 1
  • Definition 5: Interface-Aware Signal Temporal Logic