Genom3 Templates: From Middleware Independence To Formal Models Synthesis

Abstract

GenoM is an approach to develop robotic software components, which can be<br> controlled, and assembled to build complex applications. Its latest version GenoM3,<br> provides a template mechanism which is versatile enough to deploy components<br> for different middleware without any change in the specification and user code. But<br> this same template mechanism also enables us to automatically synthesize formal<br> models (for two Validation and Verification frameworks) of the final components.<br> We illustrate our approach on a real deployed example of a drone flight controller<br> for which we prove offline real-time properties, and an outdoor robot for which we<br> synthesize a controller to perform runtime verification.