Programming Safe Robotics Systems: Challenges and Advances
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)
- PDF / 4,250,655 Bytes
- 17 Pages / 439.37 x 666.142 pts Page_size
- 28 Downloads / 264 Views
University of California, Berkeley, USA [email protected] 2 Microsoft, Redmond, USA
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 Drona, a programming framework for building safe robotics systems. This paper introduces the Drona toolchain and describes how it addresses the unique challenges involved in programming safety-critical robots.
1
Introduction
Autonomous robotics systems have diverse and safety-critical roles in society today, including delivery systems, surveillance, and personal transportation. This drive towards autonomy is leading to increasing levels of software complexity. To tame this complexity and ensure safe and reliable operation of robotics systems, we have developed tools and techniques for programming and reasoning about them. In this paper, we present an overview of our work. At the heart of an autonomous robot is the specialized onboard software that must ensure safe operation without any human intervention. The robotics software stack usually consists of several interacting modules grouped into two categories: high-level controllers, taking discrete decisions and planning to ensure that the robot safely achieves complex tasks, and low-level controllers, usually consisting of closed-loop controllers and actuators that determine the robot’s continuous dynamics. The high-level controllers must react to events (inputs) from the physical world as well as other components in the software stack (Fig. 2). These controllers are therefore implemented as concurrent event-driven software. However, c Springer Nature Switzerland AG 2018 T. Margaria and B. Steffen (Eds.): ISoLA 2018, LNCS 11245, pp. 103–119, 2018. https://doi.org/10.1007/978-3-030-03421-4_8
104
A. Desai et al.
such software can be notoriously tricky to test and debug due to nondeterministic interactions with the environment and interleaving of the event handlers. We advocate writing the high-level controller in our domain-specific language P [1] which is suitable for expressing not only the asynchronous event-driven computation in the controllers but also models of other software components and the physical world (used for analysis/testing). By expressing both the controller and its environment in a si
Data Loading...
