A Verifiable and Correct-by-Construction Controller for Robot Functional Levels
This work addresses safety-critical issues for autonomous robots used in complex tasks like exploration and human assistance, though it appears incremental as an evolution of existing methodologies.
The paper tackles the challenge of ensuring safety properties like deadlock-freedom in autonomous robots by evolving the LAAS architecture with the BIP framework to create verifiable and correct-by-construction controllers for the functional level, showing through experiments that the approach is feasible and practical on real robotic platforms despite some execution overhead.
Autonomous robots are complex systems that require the interaction and cooperation between numerous heterogeneous software components. In recent times, robots are being increasingly used for complex and safety-critical tasks, such as exploring Mars and assisting/replacing humans. Consequently, robots are becoming critical systems that must meet safety properties, in particular, logical, temporal and real-time constraints. To this end, we present an evolution of the LAAS architecture for autonomous systems, in particular its GenoM tool. This evolution relies on the BIP component-based design framework, which has been successfully used in other domains such as embedded systems. We show how we integrate BIP into our existing methodology for developing the lowest (functional) level of robots. Particularly, we discuss the componentization of the functional level, the synthesis of an execution controller for it, and how we verify whether the resulting functional level conforms to properties such as deadlock-freedom. We also show through experimentation that the verification is feasible and usable for complex, real world robotic systems, and that the BIP-based functional levels resulting from our new methodology are, despite an overhead during execution, still practical on real world robotic platforms. Our approach has been fully implemented in the LAAS architecture, and the implementation has been used in several experiments on a real robot.