Soter: Programming Safe Robotics System using Runtime Assurance

Ankush Desai, Shromona Ghosh, Sanjit A. Seshia, Natarajan Shankar and Ashish Tiwari

EECS Department
University of California, Berkeley
Technical Report No. UCB/EECS-2018-127
August 21, 2018

http://www2.eecs.berkeley.edu/Pubs/TechRpts/2018/EECS-2018-127.pdf

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. 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.


BibTeX citation:

@techreport{Desai:EECS-2018-127,
    Author = {Desai, Ankush and Ghosh, Shromona and Seshia, Sanjit A. and Shankar, Natarajan and Tiwari, Ashish},
    Title = {Soter: Programming Safe Robotics System using Runtime Assurance},
    Institution = {EECS Department, University of California, Berkeley},
    Year = {2018},
    Month = {Aug},
    URL = {http://www2.eecs.berkeley.edu/Pubs/TechRpts/2018/EECS-2018-127.html},
    Number = {UCB/EECS-2018-127},
    Abstract = {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.
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.}
}

EndNote citation:

%0 Report
%A Desai, Ankush
%A Ghosh, Shromona
%A Seshia, Sanjit A.
%A Shankar, Natarajan
%A Tiwari, Ashish
%T Soter: Programming Safe Robotics System using Runtime Assurance
%I EECS Department, University of California, Berkeley
%D 2018
%8 August 21
%@ UCB/EECS-2018-127
%U http://www2.eecs.berkeley.edu/Pubs/TechRpts/2018/EECS-2018-127.html
%F Desai:EECS-2018-127