Les systèmes développés de nos jours sont de plus en plus complexes et leur fonctionnement peut avoir des
conséquences importantes sur leur environnement, voire irréversibles : systèmes avioniques, médicaux… Il est par
conséquent indispensable de garantir des systèmes sûrs, dont le fonctionnement a pu être vérifié avant leur mise en
oeuvre. L’écriture d’une spécification formelle permet non seulement une meilleure compréhension du système étudié,
mais aussi de prouver formellement, par une vérification exhaustive, son bon fonctionnement, quelle que soit
l’exécution du système.
Nos activités s’articulent autour de trois principales thématiques de recherche :
- Conception de spécifications formelles:Le développement des spécifications est une tâche
délicate, et il est facile de faire des erreurs. Le cadre des spécifications formelles oblige à une meilleure
précision, et est ici sous-jacent aux travaux qui choisissent une expression en diagrammes UML.
- Vérification paramétrée, modulaire et distribuée :La conception de nouvelles techniques de
vérification permettant de combattre le problème de l’explosion combinatoire constitue un axe majeur de nos
recherches.
- Sûreté et sécurité logicielles :L’analyse de programmes concurrents est encore balbutiante. Nous
étudions différents formalismes pour modéliser les programmes récursifs parallèles, et des techniques d’analyse
associées. Nous développons aussi différents modèles pour la détection de malware et la découverte de comportements
malveillants.
Consulter le rapport d’équipe 2017-2022 pour des
informations plus détaillées.