Vérification efficace de systèmes en temps réel

Les automates temporisés sont souvent utilisés pour modéliser des systèmes en temps réel. Le problème d'accessibilité est notamment étudié puisqu'il permet de vérifier des propriétés de sûreté mais aussi de générer des contrôleurs pour réaliser une tâche. Bien que ce problème soit déjà résolu depuis plus de 25 ans et implémenté dans plusieurs outils, nous proposons des algorithmes pour accélérer ces méthodes dans des cas particuliers.

Pour le problème de sûreté nous proposons des méthodes basées sur des abstractions de zones temporelles, surestimant les parties accessibles. Ces abstractions sont ensuite successivement raffinées grâce à une boucle CEGAR.

Pour le problème de génération de contrôleur, nous proposons des algorithmes basés sur des explorations heuristiques et A*. Nous présentons aussi des implémentations de ces algorithmes, ainsi que des résultats sur différents exemples.

La soutenance de thèse de Victor Roussanaly, de l'équipe de recherche SUMO, se déroulera le 30 novembre en salle Métivier à 14h00. Le public pourra suivre la soutenance en visio
le lien : https://webconf.lal.cloud.math.cnrs.fr/b/san-7ep-unx

Efficient verification of real-time systems.

Timed automata are often used to model real-time systems. The reachability problem is of particular interest since it allows us to check for safety properties, but also build controllers for motion planning for example. Although this problem has been solved for 25 years, and implementation of these algorithms can be found in many tools, we propose some algorithms to speed up this process in particular cases. For safety problems, we propose and test abstraction based methods, that overestimate zones of a time space that could be reachable. These abstractions are then refined successively through a CEGAR loop.

As for the problem of controller generation for motion planning, we propose algorithms based on heuristic search and A*. For all these algorithms we then show experimental results that we obtained with our implementation.
 

The defense of Victor Roussanaly, from the SUMO research team, will take place on November 30 in the Métivier room at 2:00 pm. The defense will not be open to the public but will be accessible by videoconference.
Link : https://webconf.lal.cloud.math.cnrs.fr/b/san-7ep-unx