Modeling Robot Control Architectures for Verification and Monitoring

Model-based techniques are gaining widespread adoption in Robotics for their potential in easing the production and maintenance of complex control software. One of their advantages is that the availability of models and (formal) system requirements enables automated verification of system properties at design time and the generation of monitors to guard against unwanted behaviors at operation time. To guarantee consistency between the developers’ work and the verification and monitoring results, it is mandatory to endow models with formal semantics, where the main challenge lies in striking a reasonable compromise between expressiveness and complexity of verification and monitoring.