Présentation générale
L’axe “ModélisationetVérification” s’intéresse à la modélisation, la vérification et le test des systèmes informatiques complexes. Ils développent des méthodes rigoureuses pour garantir le bon fonctionnement des systèmes. L’axe représente la conjonction de trois types d’activités de recherche :
- Une activité théorique, consistant à spécifier et étudier des formalismes variés, permettant de modéliser des systèmes critiques et d’exprimer les fonctionnalités attendues. Il s’agit de systèmes à états infinis et/ou réactifs, en particulier des systèmes distribués, temporisés, probabilistes,...,
- Une activité algorithmique, développant des outils d’analyse de systèmes critiques : vérificateurs (model-checkers) et simulateurs. Cette activité va de la conception d’algorithmes jusqu’à leur implémentation, et
- Une activité de modélisation plus pragmatique, qui a lieu dans le cadre de collaborations et de participations à des projets industriels. Longtemps limitée aux systèmes à espaces d’états finis, cette activité est en cours d’extension aux systèmes infinis (cf. AltaRica), qu’ils soient discrets ou continus (systèmes hybrides, systèmes stochastiques).
Séminaire
- Groupe de travail "Modélisation et Vérification", jeudi 11h - salle 076 LaBRI.
Contacts