Model-based Verification and Monitoring for Safe and Responsive Robots

Model-based development (MBD) is gaining widespread acceptance as a design technique in robotics. Not only it eases the work of developers and makes software deployment faster than traditional code-based approaches, but it also enables the application of formal methods without the need of specific training for developers. In particular, (off-line) automated verification is known to improve the quality of software and enable early recognition of hard-to-find bugs whereas (on-line) monitoring helps to close the reality-gap by running either on simulators or actual hardware. In this paper we present a comprehensive approach to MBD, verification, and monitoring that enables developers to design robust control software by featuring both off- and on-line checks in a push-button fashion, i.e., one where all the complexity of formal methods is hidden under the hood of the development tools.