Quang Minh TA
Titre de la thèse : Vérification légère et efficace des systèmes cyber-physiques
Les systèmes cyber-physiques sont désormais profondément intégrés dans notre quotidien, qu’il s’agisse de véhicules autonomes ou de dispositifs médicaux avancés. Comme beaucoup de ces applications sont critiques pour la sécurité, il est essentiel d’éviter tout comportement indésirable. Dans le même temps, ces systèmes sont très dynamiques et complexes, ce qui rend les méthodes de vérification traditionnelles et exhaustives peu praticables. Cela motive le recours à des techniques de vérification plus légères, capables de fonctionner efficacement et même en temps réel.
Une approche prometteuse est le monitoring, qui consiste à observer le comportement du système à travers ses traces d’exécution, plutôt que d’exiger une spécification complète de son fonctionnement interne. Cette méthode est particulièrement utile lorsque le système est trop complexe ou lorsqu’il constitue une « boîte noire » confidentielle (c’est-à-dire lorsque l’on n’a pas accès au fonctionnement interne du système). À partir de ces traces, on peut vérifier si le système respecte certaines règles. Par exemple : une pompe à insuline doit délivrer de l’insuline pour maintenir le taux de glucose en dessous d’un seuil (éventuellement exprimé comme paramètre inconnu), sauf si le rythme cardiaque du patient dépasse un autre seuil ; dans ce cas, l’injection doit s’interrompre en moins d’une seconde.
Ce projet de thèse vise à développer de nouvelles manières d’exprimer de telles règles complexes, à concevoir des algorithmes et structures de données efficaces pour le monitoring, et à implémenter ces solutions dans des logiciels. Les méthodes seront évaluées sur des benchmarks et appliquées à des études de cas réalistes, afin de contribuer à des technologies plus fiables.
Thesis title : Efficient lightweight verification of cyber-physical systems
Cyber-physical systems are now deeply integrated into our lives, from autonomous vehicles to advanced medical devices. Because many of these applications are safety-critical, preventing undesired behavior is essential. At the same time, these systems are highly dynamic and complex, which makes traditional, exhaustive verification methods impractical. This motivates the need for lightweight verification techniques that can operate efficiently and even in real time.
One promising approach is monitoring, which observes the system’s behavior through its execution traces rather than requiring full specification of its internal design. This is crucial when the system is too complex, or is a black box, i.e., a system whose internal behavior is unknown. Based on these traces, we can check whether the system complies with desired rules. For example: an insulin pump should deliver insulin to keep blood glucose below a threshold (possibly expressed as an unknown parameter), except if the patient’s heart rate exceeds another threshold, in which case the pump must stop within one second.
This PhD project aims to develop new ways to express such complex rules, design efficient algorithms and data structures for monitoring, and implement these solutions in software. The methods will be evaluated on benchmarks and applied to realistic case studies, ultimately contributing to more reliable technologies.
Contactez-nous !
Campus de Villetaneuse
@univ_SPN