GenoM3 Templates: from Middleware Independence to Formal Models Synthesis
This work addresses the problem of improving reliability and flexibility in robotic software development for researchers and engineers, though it appears incremental by building on the existing GenoM approach.
The authors tackled the challenge of developing versatile robotic software components by introducing GenoM3 templates, which enable middleware-independent deployment and automatic synthesis of formal models for validation and verification, as demonstrated on a drone flight controller with proven real-time properties and an outdoor robot for runtime verification.
GenoM is an approach to develop robotic software components, which can be controlled, and assembled to build complex applications. Its latest version GenoM3, provides a template mechanism which is versatile enough to deploy components for different middleware without any change in the specification and user code. But this same template mechanism also enables us to automatically synthesize formal models (for two Validation and Verification frameworks) of the final components. We illustrate our approach on a real deployed example of a drone flight controller for which we prove offline real-time properties, and an outdoor robot for which we synthesize a controller to perform runtime verification.