Description
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. SOTER 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. SOTER 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 SOTER-enabled RTA ensures safety of the system, including when untrusted third-party components have bugs or deviate from the desired behavior.