Establishing A-Priori Performance Guarantees for Robot Missions that Include Localization Software

1. Introduction

For systems that need to function in critical situations, such as in healthcare applications, search and rescue robotics, and automated counter weapons of mass destructions (CWMD) missions, it is crucially important that the system function as specified or the result might be loss of life, or property damage or both. One approach to this problem is to monitor the system in operation (Leucker & Schallhart, 2009) and to signal an alert to a supervisor of the system when the performance is going, or predicted to go, outside the necessary performance envelope. This monitoring approach can be very effective in cases where a supervisor can step in, or the system can be disabled without consequence, when a performance problem is observed. However, in the case that the system is autonomous, or the supervisor cannot interact sufficiently quickly and the system cannot simply be disabled, then an alternate approach is necessary. In previous work for the Defense Threat Reduction Agency (Lyons et al., 2015) we have developed an efficient approach to the automatic, a-priori determination of performance guarantees for behavior-based robot missions operating in uncertain environments.

This work is related to formal software verification (Jhala & Majumdar, 2009) (DeMoura & Bjorner, 2012): a design tool to determine whether a piece of software will function properly without having to execute the software. The field has progressed strongly in recent years with developments in model-checking (Jhala & Majumdar, 2009) and satisfiability (SMT) engines (DeMoura & Bjorner, 2012). However, all such methods can at best approximate real robot performance because of the undecidability of the underlying verification problem. Designing a verification approach for mission critical robot software requires understanding what aspects of the robot software are of most importance to the problem. Behavior-based robot programming (Arkin, 1998) is an important tool in autonomous robotics that yields robot programs that are robust to uncertainty about exactly what environment the robots will face during execution. For this reason, in recent work (Lyons et al., 2015), we addressed the problem of automatically verifying behavior-based robot programs by leveraging the structure of such programs. The approach employs a unique combination of static analysis techniques and probabilistic reasoning to provide performance guarantees for behavior-based robot programs operating in physical environments with uncertain knowledge about obstacles to motion. Rather than addressing computational verification problems such as absence of deadlock or absence of run-time errors (Trojanek & Eder, 2014) (Walter, Taubig, & Luth, 2010), or verifying software generated control signals without consideration of the physical platform (Kim, Kang, & Lee, 2005), our work focuses on establishing performance guarantees for the mission software with a model of an uncertainly-known physical environment.