Programming safe robotics systems: Challenges and advances

Abstract

A significant challenge for large-scale deployment of autonomous mobile robots is to program them with formal guarantees and high assurance of correct operation. Our approach towards enabling safe programming of robotics system consists of two parts: (1) a programming language for implementing, specifying, and compositionally (assume-guarantee) testing the high-level reactive robotics software; (2) a runtime assurance system to ensure that the assumptions used during design-time testing of high-level software hold at runtime. Combining high-level programming language and its systematic testing with runtime enforcement helps us bridge the gap between software testing that makes assumptions about the low-level controllers and the physical world, and the actual execution of the software on a real robotic platform in the physical world. We implement our approach in, a programming framework for building safe robotics systems. This paper introduces the toolchain and describes how it addresses the unique challenges involved in programming safety-critical robots.