We gratefully acknowledge support from
the Simons Foundation and member institutions.
Full-text links:

Download:

Current browse context:

cs

Change to browse by:

References & Citations

DBLP - CS Bibliography

Bookmark

(what is this?)
CiteULike logo BibSonomy logo Mendeley logo del.icio.us logo Digg logo Reddit logo ScienceWISE logo

Computer Science > Robotics

Title: Monitoring ROS2: from Requirements to Autonomous Robots

Authors: Ivan Perez (KBR at NASA Ames Research Center), Anastasia Mavridou (KBR at NASA Ames Research Center), Tom Pressburger (NASA Ames Research Center), Alexander Will (Virginia Commonwealth University), Patrick J. Martin (Virginia Commonwealth University)
Abstract: Runtime verification (RV) has the potential to enable the safe operation of safety-critical systems that are too complex to formally verify, such as Robot Operating System 2 (ROS2) applications. Writing correct monitors can itself be complex, and errors in the monitoring subsystem threaten the mission as a whole. This paper provides an overview of a formal approach to generating runtime monitors for autonomous robots from requirements written in a structured natural language. Our approach integrates the Formal Requirement Elicitation Tool (FRET) with Copilot, a runtime verification framework, through the Ogma integration tool. FRET is used to specify requirements with unambiguous semantics, which are then automatically translated into temporal logic formulae. Ogma generates monitor specifications from the FRET output, which are compiled into hard-real time C99. To facilitate integration of the monitors in ROS2, we have extended Ogma to generate ROS2 packages defining monitoring nodes, which run the monitors when new data becomes available, and publish the results of any violations. The goal of our approach is to treat the generated ROS2 packages as black boxes and integrate them into larger ROS2 systems with minimal effort.
Comments: In Proceedings FMAS2022 ASYDE2022, arXiv:2209.13181
Subjects: Robotics (cs.RO); Computation and Language (cs.CL); Formal Languages and Automata Theory (cs.FL)
ACM classes: D.2.1; D.2.4; I.2.9;
Journal reference: EPTCS 371, 2022, pp. 208-216
DOI: 10.4204/EPTCS.371.15
Cite as: arXiv:2209.14030 [cs.RO]
  (or arXiv:2209.14030v1 [cs.RO] for this version)

Submission history

From: EPTCS [view email]
[v1] Wed, 28 Sep 2022 12:19:13 GMT (583kb,D)

Link back to: arXiv, form interface, contact.