Modular Verification of Autonomous Space Robotics
This addresses the critical need to prevent software failures in space missions, which can lead to mission loss and endanger astronauts and equipment, though it is incremental in integrating existing verification approaches.
The paper tackles the problem of verifying autonomous space robot control software by introducing a method that integrates various verification techniques through First-Order Logic specifications, which guide verification of individual nodes and measure overall system confidence.
Ensuring that autonomous space robot control software behaves as it should is crucial, particularly as software failure in space often equates to mission failure and could potentially endanger nearby astronauts and costly equipment. To minimise mission failure caused by software errors, we can utilise a variety of tools and techniques to verify that the software behaves as intended. In particular, distinct nodes in a robotic system often require different verification techniques to ensure that they behave as expected. This paper introduces a method for integrating the various verification techniques that are applied to robotic software, via a First-Order Logic (FOL) specification that captures each node's assumptions and guarantees. These FOL specifications are then used to guide the verification of the individual nodes, be it by testing or the use of a formal method. We also outline a way of measuring our confidence in the verification of the entire system in terms of the verification techniques used.