Vérification à l'exécution efficace pour les systèmes temps-réel – ERVoRS

Les systèmes temps-réel (STR), tels que les voitures et les robots mobiles, sont omniprésents. Une question fondamentale est la suivante : un STR se comportera-t-il comme prévu ? La vérification formelle étudie cette question en analysant un modèle mathématique du STR, reposant sur un formalisme temporisé p.ex les automates temporisés, contre des propriétés formalisées dans une logique temporisée. Typiquement, la vérification formelle se réalise hors ligne, c.à.d avant le déploiement du STR. Tel est le cas du model checking, où tous les comportements possibles capturés par le modèle du STR sont vérifiés contre les propriétés d'intérêt. Bien que cette exhaustivité d'analyse rende le model checking pertinent pour les STR critiques (où la violation d'une propriété peut entraîner des dégâts catastrophiques), elle est la source du fameux problème de l'explosion combinatoire de l'espace d'états en pratique. La vérification à l'exécution, en revanche, ne requiert pas d'exploration exhaustive de l'espace d'états à priori; elle se fait via le monitoring (observation du RTS vis-à-vis une propriété) et éventuellement la récupération (intervention en cas de violation de la propriété) au fur et à mesure de l'exécution. Cependant, malgré de grandes avancées, cette discipline demeure inadaptée aux STR critiques. En particulier, il y a un manque de théorie compréhensive, et ainsi d'outils qui vont avec, pour un monitoring et une récupération efficaces dans le cadre temporisé. Le but d'ERVoRS est de faire avancer l'état de l'art de la vérification à l'exécution en (i) répondant à des questions théoriques, p.ex quelles sont les propriétés temporisées monitorables ? Ou encore comment quantifier et réduire les overheads du monitoring et de la récupération ? Et (ii) complémentant les réponses à ces questions par des implémentations efficaces évaluées sur des cas d'études réels complexes.