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.