Symbolic Fault Injection for Plan-based Robotics

Autonomous robots are being used increasingly in safety-critical environments. Due to their dynamic nature and uncertainty, failures of low-level actions are common. In plan-based robotics, these failures are handled inside the higher-level plans, using a multitude of failure handling strategies. With the increasing complexity of robotic plans, failures may be accidentally left unhandled. This will usually stop the plan entirely. To avoid such a situation, the failure handling should ideally be complete, i.e. there should be no failure that can reach the top-level of the execution. In this paper, we propose to use formal methods, in particular symbolic fault injection to tackle the problem of finding unhandled failures or proving that no such failure exists. We implement symbolic fault injection for the CRAM Planning Language (CPL). We base our work on the worst-case assumption that any low-level action may fail at any time with any of its possible types of failure. Our work builds upon an existing symbolic execution engine for CPL and extends it to reason about CPL’s failure handling mechanism. We also present a way to implement the worst-case assumption directly into CPL. Our experimental evaluation suggests that symbolic fault injection is a suitable and scalable method to find unhandled failures in robotic plans.