A Compositional Approach to Verifying Modular Robotic Systems
- URL: http://arxiv.org/abs/2208.05507v2
- Date: Thu, 30 Nov 2023 17:02:05 GMT
- Title: A Compositional Approach to Verifying Modular Robotic Systems
- Authors: Matt Luckcuck and Marie Farrell and Angelo Ferrando and Rafael C.
Cardoso and Louise A. Dennis and Michael Fisher
- Abstract summary: This paper describes a compositional approach to specifying the nodes in robotic systems built using the Robotic Operating System (ROS)
We introduce inference rules that facilitate the composition of these node-level contracts to derive system-level properties.
We also present a novel Domain-Specific Language, the ROS Contract Language, which captures a node's FOL specification and links this contract to its implementation.
- Score: 1.385411134620987
- License: http://creativecommons.org/licenses/by/4.0/
- Abstract: Robotic systems used in safety-critical industrial situations often rely on
modular software architectures, and increasingly include autonomous components.
Verifying that these modular robotic systems behave as expected requires
approaches that can cope with, and preferably take advantage of, this inherent
modularity. This paper describes a compositional approach to specifying the
nodes in robotic systems built using the Robotic Operating System (ROS), where
each node is specified using First-Order Logic (FOL) assume-guarantee contracts
that link the specification to the ROS implementation. We introduce inference
rules that facilitate the composition of these node-level contracts to derive
system-level properties. We also present a novel Domain-Specific Language, the
ROS Contract Language, which captures a node's FOL specification and links this
contract to its implementation. RCL contracts can be automatically translated,
by our tool Vanda, into executable monitors; which we use to verify the
contracts at runtime. We illustrate our approach through the specification and
verification of an autonomous rover engaged in the remote inspection of a
nuclear site, and finish with smaller examples that illustrate other useful
features of our framework.
Related papers
- Complex Event Recognition with Symbolic Register Transducers: Extended Technical Report [51.86861492527722]
We present a system for Complex Event Recognition based on automata.
Our system is based on an automaton model which is a combination of symbolic and register automata.
We show how SRT can be used in CER in order to detect patterns upon streams of events.
arXiv Detail & Related papers (2024-07-03T07:59:13Z) - ROS-LLM: A ROS framework for embodied AI with task feedback and structured reasoning [74.58666091522198]
We present a framework for intuitive robot programming by non-experts.
We leverage natural language prompts and contextual information from the Robot Operating System (ROS)
Our system integrates large language models (LLMs), enabling non-experts to articulate task requirements to the system through a chat interface.
arXiv Detail & Related papers (2024-06-28T08:28:38Z) - Protocols to Code: Formal Verification of a Next-Generation Internet Router [9.971817718196997]
SCION routers run a cryptographic protocol for secure packet forwarding in an adversarial environment.
We verify both the protocol's network-wide security properties and low-level properties of its implementation.
This paper explains our approach, summarizes the main results, and distills lessons for the design and implementation of verifiable systems.
arXiv Detail & Related papers (2024-05-09T19:57:59Z) - Correct-by-Construction Design of Contextual Robotic Missions Using
Contracts [6.890369837091434]
We propose a novel compositional framework for specifying and implementing contextual robotic missions.
The mission specification is structured in a hierarchical and modular fashion, allowing for each sub-mission to be synthesized as an independent robot controller.
arXiv Detail & Related papers (2023-06-13T21:29:17Z) - Monitoring ROS2: from Requirements to Autonomous Robots [58.720142291102135]
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.
arXiv Detail & Related papers (2022-09-28T12:19:13Z) - Safe RAN control: A Symbolic Reinforcement Learning Approach [62.997667081978825]
We present a Symbolic Reinforcement Learning (SRL) based architecture for safety control of Radio Access Network (RAN) applications.
We provide a purely automated procedure in which a user can specify high-level logical safety specifications for a given cellular network topology.
We introduce a user interface (UI) developed to help a user set intent specifications to the system, and inspect the difference in agent proposed actions.
arXiv Detail & Related papers (2021-06-03T16:45:40Z) - Neural Network-based Control for Multi-Agent Systems from
Spatio-Temporal Specifications [0.757024681220677]
We use Spatio-Temporal Reach and Escape Logic (STREL) as a specification language.
We map control synthesis problems with STREL specifications to propose a combination of gradient and gradient-based methods to solve such problems.
We develop a machine learning technique that uses the results of the off-line optimizations to train a neural network that gives the control inputs current states.
arXiv Detail & Related papers (2021-04-06T18:08:09Z) - Symbolic Reinforcement Learning for Safe RAN Control [62.997667081978825]
We show a Symbolic Reinforcement Learning (SRL) architecture for safe control in Radio Access Network (RAN) applications.
In our tool, a user can select a high-level safety specifications expressed in Linear Temporal Logic (LTL) to shield an RL agent running in a given cellular network.
We demonstrate the user interface (UI) helping the user set intent specifications to the architecture and inspect the difference in allowed and blocked actions.
arXiv Detail & Related papers (2021-03-11T10:56:49Z) - SOTER on ROS: A Run-Time Assurance Framework on the Robot Operating
System [5.358161704743753]
SOTER is a run-time assurance framework for building safe distributed mobile robotic systems.
We show that SOTER enabled systems ensure safety, even when using unknown and untrusted components.
arXiv Detail & Related papers (2020-08-21T22:48:26Z) - Towards an Interface Description Template for AI-enabled Systems [77.34726150561087]
Reuse is a common system architecture approach that seeks to instantiate a system architecture with existing components.
There is currently no framework that guides the selection of necessary information to assess their portability to operate in a system different than the one for which the component was originally purposed.
We present ongoing work on establishing an interface description template that captures the main information of an AI-enabled component.
arXiv Detail & Related papers (2020-07-13T20:30:26Z)
This list is automatically generated from the titles and abstracts of the papers in this site.
This site does not guarantee the quality of this site (including all information) and is not responsible for any consequences.