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

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

Damian Lyons (Department of Computer and Information Science, Fordham University, New York City, NY, USA), Ronald C. Arkin (Georgia Institute of Technology, Atlanta, GA, USA), Shu Jiang (Georgia Institute of Technology, Atlanta, GA, USA), Matthew J. O'Brien (Georgia Institute of Technology, Atlanta, GA, USA), Feng Tang (Fordham University, New York City, NY, USA) and Peng Tang (Fordham University, New York City, NY, USA)
DOI: 10.4018/IJMSTR.2017010103

Abstract

One approach to determining whether an automated system is performing correctly is to monitor its performance, signaling when the performance is not acceptable; another approach is to automatically analyze the possible behaviors of the system a-priori and determine performance guarantees. Thea authors have applied this second approach to automatically derive performance guarantees for behavior-based, multi-robot critical mission software using an innovative approach to formal verification for robotic software. Localization and mapping algorithms can allow a robot to navigate well in an unknown environment. However, whether such algorithms enhance any specific robot mission is currently a matter for empirical validation. Several approaches to incorporating pre-existing software into the authors' probabilistic verification framework are presented, and one used to include Monte-Carlo based localization software. Verification and experimental validation results are discussed for real localization missions with this software, showing that the proposed approach accurately predicts performance.
Article Preview

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.

Complete Article List

Search this Journal:
Reset
Open Access Articles: Forthcoming
Volume 7: 2 Issues (2019): Forthcoming, Available for Pre-Order
Volume 6: 2 Issues (2018): Forthcoming, Available for Pre-Order
Volume 5: 4 Issues (2017): 3 Released, 1 Forthcoming
Volume 4: 4 Issues (2016)
Volume 3: 4 Issues (2015)
Volume 2: 4 Issues (2014)
Volume 1: 4 Issues (2013)
View Complete Journal Contents Listing