A Formal Safety Net for Waypoint-Following in Ground Robots

被引:20
作者
Bohrer, Brandon [1 ,2 ]
Tan, Yong Kiam [2 ]
Mitsch, Stefan [2 ]
Sogokon, Andrew [2 ]
Platzer, Andre [1 ,2 ]
机构
[1] Tech Univ Munich, Fak Informat, D-85748 Garching, Germany
[2] Carnegie Mellon Univ, Comp Sci Dept, Pittsburgh, PA 15213 USA
关键词
Formal methods in robotics and automation; robot safety; hybrid logical/dynamical planning and verification; motion control; kinematics; TEMPORAL LOGIC; VERIFICATION; SYSTEMS;
D O I
10.1109/LRA.2019.2923099
中图分类号
TP24 [机器人技术];
学科分类号
080202 ; 1405 ;
摘要
We present a reusable formally verified safety net that provides end-to-end safety and liveness guarantees for two-dimensional way point-following of Dubins-type ground robots with tolerances and acceleration. First, we model a robot in differential dynamic logic and specify assumptions on the controller and robot kinematics. Second, we prove formal safety and liveness properties for waypoint-following with speed limits. Third, we synthesize a monitor, which is automatically proven to enforce model compliance at runtime. Fourth, our use of the VeriPhy toolchain makes these guarantees carry over down to the level of machine code with untrusted controllers, environments, and plans. The guarantees for the safety net apply to any robot as long as the waypoints are chosen safely and the physical assumptions in its model hold. Experiments show that these assumptions hold in practice, with an inherent tradeoff between compliance and performance.
引用
收藏
页码:2910 / 2917
页数:8
相关论文
共 25 条
[1]   Online Verification of Automated Road Vehicles Using Reachability Analysis [J].
Althoff, Matthias ;
Dolan, John M. .
IEEE TRANSACTIONS ON ROBOTICS, 2014, 30 (04) :903-918
[2]  
[Anonymous], 2010, EMSOFT
[3]  
[Anonymous], 2017, FSR
[4]  
Bohrer B, 2018, ACM SIGPLAN NOTICES, V53, P617, DOI [10.1145/3192366.3192406, 10.1145/3296979.3192406]
[5]   A Benchmark Suite for Hybrid Systems Reachability Analysis [J].
Chen, Xin ;
Schupp, Stefan ;
Ben Makhlouf, Ibtissem ;
Abraham, Erika ;
Frehse, Goran ;
Kowalewski, Stefan .
NASA FORMAL METHODS (NFM 2015), 2015, 9058 :408-414
[6]   Combining Model Checking and Runtime Verification for Safe Robotics [J].
Desai, Ankush ;
Dreossi, Tommaso ;
Seshia, Sanjit A. .
RUNTIME VERIFICATION (RV 2017), 2017, 10548 :172-189
[7]   Temporal logic motion planning for dynamic robots [J].
Fainekos, Georgios E. ;
Girard, Antoine ;
Kress-Gazit, Hadas ;
Pappas, George J. .
AUTOMATICA, 2009, 45 (02) :343-352
[8]  
Filippidis Ioannis, 2016, 2016 IEEE Conference on Control Applications (CCA), P1030, DOI 10.1109/CCA.2016.7587949
[9]   LTLMoP: Experimenting with Language, Temporal Logic and Robot Control [J].
Finucane, Cameron ;
Jing, Gangyuan ;
Kress-Gazit, Hadas .
IEEE/RSJ 2010 INTERNATIONAL CONFERENCE ON INTELLIGENT ROBOTS AND SYSTEMS (IROS 2010), 2010, :1988-1993
[10]   The dynamic window approach to collision avoidance [J].
Fox, D ;
Burgard, W ;
Thrun, S .
IEEE ROBOTICS & AUTOMATION MAGAZINE, 1997, 4 (01) :23-33