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

Type de soutenance
Thèse
Date de début
Date de fin
Lieu
IRISA Rennes
Salle
Métivier
Orateur
Victor Roussanaly (SUMO)
Département principal
Sujet

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

Composition du jury
Olivier H. Roux - Professeur LS2N / École Centrale de Nantes - Président du jury
Étienne André - Professeur, Université de Lorraine - Rapporteur
Thao Dang (Grenoble) - DR CNRS, Verimag - Rapportrice
B. Srivathsan - Associate professor, Chennai Mathematical Institute - Examinateur
Frédéric Herbreteau (Bordeaux) - MCF, Univ. Bordeaux – Examinateur
Directeur et co-encadrant de Thèse :
Nicolas Markey - DR CNRS - IRISA, équipe SUMO, Rennes
Ocan Sankur - CR CNRS - IRISA, équipe SUMO, Rennes