SOTER: A Runtime Assurance Framework for Programming Safe Robotics Systems

被引:51
作者
Desai, Ankush [1 ]
Ghosh, Shromona [1 ]
Seshia, Sanjit A. [1 ]
Shankar, Natarajan [2 ]
Tiwari, Ashish [2 ,3 ]
机构
[1] Univ Calif Berkeley, Berkeley, CA 94720 USA
[2] SRI Int, 333 Ravenswood Ave, Menlo Pk, CA 94025 USA
[3] Microsoft, Redmond, WA USA
来源
2019 49TH ANNUAL IEEE/IFIP INTERNATIONAL CONFERENCE ON DEPENDABLE SYSTEMS AND NETWORKS (DSN 2019) | 2019年
基金
美国国家科学基金会;
关键词
COLLISION;
D O I
10.1109/DSN.2019.00027
中图分类号
TP3 [计算技术、计算机技术];
学科分类号
0812 ;
摘要
The recent drive towards achieving greater autonomy and intelligence in robotics has led to high levels of complexity. 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 these challenges, we present SOTER, a robotics programming framework with two key components: (1) a programming language for implementing and testing high-level reactive robotics software, and (2) an integrated runtime assurance (RTA) system that helps enable the use of uncertified components, while still providing safety guarantees. SOTER provides language primitives to declaratively construct a RTA module consisting of an advanced, high-performance controller (uncertified), a safe, lower-performance controller (certified), and the desired safety specification. The framework provides a formal guarantee that a well-formed RTA module always satisfies the safety specification, without completely sacrificing performance by using higher performance uncertified components whenever safe. SOTER allows the complex robotics software stack to be constructed as a composition of RTA modules, where each uncertified component is protected using a RTA module. 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 the SOTER-enabled RTA ensures the safety of the system, including when untrusted third-party components have bugs or deviate from the desired behavior.
引用
收藏
页码:138 / 150
页数:13
相关论文
共 53 条
[1]   Rigorous design of robot software: A formal component-based approach [J].
Abdellatif, Tesnim ;
Bensalem, Saddek ;
Combaz, Jacques ;
de Silva, Lavindra ;
Ingrand, Felix .
ROBOTICS AND AUTONOMOUS SYSTEMS, 2012, 60 (12) :1563-1578
[2]  
Akametalu AK, 2014, IEEE DECIS CONTR P, P1424, DOI 10.1109/CDC.2014.7039601
[3]   Reactive modules [J].
Alur, R ;
Henzinger, TA .
FORMAL METHODS IN SYSTEM DESIGN, 1999, 15 (01) :7-48
[4]  
[Anonymous], 2016, ARXIV E PRINTS
[5]  
[Anonymous], P 18 INT C AUT PLANN
[6]  
[Anonymous], 2017, 3D ROBOTICS
[7]  
[Anonymous], 2009, IEEE T ROBOTICS
[8]  
[Anonymous], 2017, PX4 AUTOPILOT
[9]   Provably safe and robust learning-based model predictive control [J].
Aswani, Anil ;
Gonzalez, Humberto ;
Sastry, S. Shankar ;
Tomlin, Claire .
AUTOMATICA, 2013, 49 (05) :1216-1226
[10]  
Aswani A, 2012, P AMER CONTR CONF, P4661