Performance verification for robot missions in uncertain environments

Establishing a-priori mission performance guarantees is crucial if autonomous robots are to be used with confidence in missions where failure could incur high costs in life and property damage. Automatic mission software verification, in addition to simulation and experimental benchmarking, is a key component of the solution for establishing performance guarantees. This component requires automatically verifying that the software constructed by the mission designer when executed in a partially known environment will adhere to the performance guarantee. In prior work we developed VIPARS, a unique approach to verifying performance guarantees for autonomous behavior-based robot software based on a combination of static analysis and Bayesian networks. While that approach produced fast and accurate verification of single robot missions with robot motion uncertainty, it did not address multiple-robot missions or any form of uncertainty related to environment geometry. This paper addresses the challenges involved in building a software tool for verifying the behavior of a multi-robot waypoint mission that includes uncertainly located obstacles and uncertain environment geometry as well as uncertainty in robot motion. An approach is presented to the problem of a-priori specification of uncertain environments for robot program verification. Two approaches to modeling probabilistic localization for verification are presented: a high-level approach and an approach that allows run-time localization code to be embedded in verification. Verification and experimental validation results are presented for several autonomous robot missions, demonstrating the accuracy of verification and the mission-specific benefit of localization (C) 2017 Elsevier B.V. All rights reserved.