Modelling, verification and test of high-level robotic plans

Abstract

Robots are an integral part of current industrial processes. Typical industrial robots are used in different factory settings to handle repetitive tasks and thus ease the workload for human workers. Recent advances in technology and artificial intelligence opened the door for a generation of more mobile, flexible and autonomous robots for a wider variety of applications. The combination of dynamic environments, complex tasks and a need for explainability call for a structured, high-level approach to autonomous robotics. One such approach is plan-based robotics, where a high-level plan is responsible for the orchestration and supervision of lower-level modules such as a motion planner, knowledge base or computer vision module. The plan itself is written in a high-level plan language. With the increasing complexity of robotic plans, programming errors and oversights only become more likely. There is an undeniable need for a high level of safety, robustness and correctness in autonomous robots. This requires not only a thorough engineering of the robotic software, but also techniques to assess the correctness, and to uncover hidden bugs. In this thesis, we aim to extend the state-of-the-art in verification techniques for high-level robotic plans. We present both formal and test-based methods. In particular, we make contributions to three areas of robotic plan verification. First, we present several techniques for the symbolic verification of high-level robotic plans. Our second contribution is the development of two approaches that aid in the modelling of robotic environments and thus facilitate both the planning and verification process. Finally, we present coverage-guided fuzzing as an automatic, test-based method for bug-finding in robotic plans. All of our contributions are applied to the CRAM Plan Language (CPL). They are described in detail and experimentally evaluated to demonstrate their effectiveness.