SOTER: Programming Safe Robotics System using Runtime Assurance

Autonomous robots increasingly depend on third-party off-the-shelf components and complex machine-learning techniques. This trend makes it challenging to provide strong design-time certification of correct operation. To address this challenge, we present SOTER, a programming framework that integrates the core principles of runtime assurance to enable the use of uncertified controllers, while still providing safety guarantees. Runtime Assurance (RTA) is an approach used for safety-critical systems where design-time analysis is coupled with run-time techniques to switch between unverified advanced controllers and verified simple controllers. In this paper, we present a runtime assurance programming framework for modular design of provably-safe robotics software. \tool provides language primitives to declaratively construct a \rta module consisting of an advanced controller (untrusted), a safe controller (trusted), and the desired safety specification (S). If the RTA module is well formed then the framework provides a formal guarantee that it satisfies property S. The compiler generates code for monitoring system state and switching control between the advanced and safe controller in order to guarantee S. RTA allows complex systems to be constructed through the composition of RTA modules. To demonstrate the efficacy of our framework, we consider a real-world case-study of building a safe drone surveillance system. Our experiments both in simulation and on actual drones show that RTA-enabled RTA ensures safety of the system, including when untrusted third-party components have bugs or deviate from the desired behavior.