Modélisation & Vérification
Responsable : Laurent Simon .

Présentation générale

Le thème MV représente la continuation des activités de recherche de l'équipe MVTsi, créée début des années quatre-vingt par André Arnold. Ses membres se consacrent à 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. Le thème 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.
  • 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), soit discrets, ou continus (systèmes hybrides, systèmes stochastiques).

Séminaire

Logiciels

  • AltaRica: language and tools for modelling and verification.
  • FASTer: a tool dedicated to the analysis of infinite systems.
  • Insight: binary program analysis framework.

Projets

  • SAFE, projet UE, 2011--.
  • VACSIM (Validation de la commande des systèmes critiques par couplage simulation et méthodes d'analyse formelle), ANR 2011-2015.
  • MARSHAL, projet FUI (Fonds Unique Interministériel), 2012-2014.
  • REACHARD (Taming Hard Reachability Problems for Counter Systems), ANR BLANC (SIMI 2), 2011-2014.
  • FREC (Frontiers of recognizability), ANR BLANC, 2010-2013.
  • GAMES (Games for Design and Verification) ESF Research Networking Programme, 2008-2012.
  • BINCOA (Symbolic Methods for BINary Code Analysis), ANR ARPEGE, 2009-2012.
  • AVeriSS (Automated Verification of Software Systems), ANR "Sécurité et Informatique", 2007-2010.
  • DocFlow (Analysis, monitoring and optimisation of Web documents and services), ANR "Masse de Données et Connaissances Ambiantes" 2007-2009.
  • DOTS (Distributed Open and Timed Systems), ANR "Sécurité et Informatique" 2007--2010.
  • SPaCIFY (Ingénierie des modèles et méthodes formelles intégrées pour le développement des logiciels de vol spatiaux), ANR "Technologies logicielles", 2007-2009.
  • GAMES (Games for Design and Verification) ESF Research Networking Programme, 2008-2012.
  • BINCOA (Symbolic Methods for BINary Code Analysis), ANR ARPEGE, 2009-2011.
Page mise à jour le 08/02/2016 à 09:34