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, and its tool GenoM. 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 feasible for 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.
A Verifiable and Correct-by-Construction Controller for Robot Functional Levels
2011-09-01
doi:10.6092/JOSER_2011_02_01_p1
Aufsatz (Zeitschrift)
Elektronische Ressource
Englisch
DDC: | 629 |
Verifiable L1 Adaptive Controller for Aerial Refueling
AIAA | 2007
|Correct-by-Construction Controller Synthesis for Safety-Critical Systems
TIBKAT | 2024
|Verifiable L1 Adaptive Controller for Aerial Refueling AIAA Paper
British Library Conference Proceedings | 2007
|AIAA-2006-6416 Theoretically Verifiable Stability Margins for an Adaptive Controller
British Library Conference Proceedings | 2006
|