Introduction

Literature Review

• RTA is architecture is defined on Simplex:
  • Advanced controller operating in nominal operating conditions
  • Safe controller that can be pre-certified to keep robot within region of safe operation
  • Decision module which is pre-certified to periodically monitor controller state and switch from AC to SC
• According to article, existing techniques apply RTA to:
  • single untrusted component in the system, or
  • wrap large monolithic system into a single instance of Simplex making verification difficult or infeasible.

Contributions

• SOTER addresses existing limitations to RTA frameworks.
  • Programming framework for building safe robotic systems using RTA
  • It is a collection of periodic processes (nodes) that interact with each other using a publish-subscribe model of communication like Robot Operating System (ROS).
  • RTA module in SOTER consists of AC node, SC node and safety specification. If module is well formed then framework provides guarantee that system satisfies the safety specs.
• Contributions:
  • Programming framework for Simplex-based RTA systems with language primitives for modular design of safe robotics systems.
  • Theoretical formalism based on computing reachable sets that keep system provably safe while maintaining smooth switching behaviour between AC and SC.
  • Framework for modular design for RTA

Definition

A well formed RTA Module $M=(N_{ac},N_{sc},N_{DM},\mathrm{\Delta },{\varphi }_{safe},{\varphi }_{safer})$ where:

• $N$ = Node
• $\mathrm{\Delta }$ = Time between checks
• $\varphi$ = Invariant conditions
  Is defined such that:
• Maximum period of each node is $\mathrm{\Delta }$ with Decision Module running for the full duration and the other nodes being less than or equal to it.
• Output topics of the AC and SC nodes is the same.
• Safety: The reachability of system using SC will always satisfy the "safe" conditions.
• Liveness: From every state in the "safe" condition, after some finite time the system is guaranteed to stay in the "safer" condition for at least the time period $\mathrm{\Delta }$.
• Irrespective of controller, if we start from state in "safer" condition, we will remain in "safe" condition for at least twice the period $\mathrm{\Delta }$.

Notes

• The AC can be a blackbox, but must be able to reason about SC and DM.
• Defining the value of $\mathrm{\Delta }$ determines how conservative the system will behave.
  • Can apply concept of time-to-failure to identify the maximum allowable time period of sampling.