Equipe de recherche FORMES

Méthodes Formelles pour les Systèmes Embarqués

Présentation de l'équipe

FORMES est une équipe du LIAMA réunissant des chercheurs de l'INRIA et des universités de Tsinghua et Beihang. Les recherches réalisées en son sein ont pour but d'aider au développement d'applications embarquées sures et fiables, en exploitant les synergies entre deux approches différentes, d'une part la simulation de hardware en temps réel, et d'autre part le développement de preuves formelles.

Axes de recherche

L'équipe FORMES s'attaque aux défis du développement de systèmes embarqués avec une nouvelle approche, combinant des techniques de simulation de hardware très rapide avec des méthodes formelles avancées, dans le but de prouver des propriétés qualitatives et quantitatives du système final. Cette approche nécessite la construction d'un environnement de simulation et des outils pour l'analyse des simulations et la preuve du système simule. Nous devons donc connecter des outils de simulation avec des analyseurs de code et des assistants de preuve pour accomplir les tâches suivantes :
  • Améliorer les techniques de simulation de hardware pour augmenter la vitesse de simulation et produire des représentations des programmes adaptées a l'analyse et la preuve formelle ;
  • Appliquer des outils de validation et de preuve aux traces obtenues par simulation ;
  • Etendre et améliorer les techniques de preuve formelle et les assistants de preuve de facon à pouvoir traiter des programmes embarqués ou leur simulation.

Logiciels

Relations industrielles et internationales

  • L'équipe FORMES est commune avec l'Université de Tsinghua où elle est localisée avec l'Université d'Aéronautique de Pékin et l'Université des Sciences et Technologies de Pékin.
  • L'équipe FORMES coordonne le projet franco-chinois SIVES supporté par l'ANR en France et la NSF en Chine, entre l'INRIA et les Universités de Tsinghua et Beihang.
  • La partie du projet dédiée à la simulation est sponsorisée par Schneider Electric China.

Mots-clés : Methodes formelles Preuve Coq Certification Systemes embarques Simulation Compilation

Equipes de recherche du même thème :

Siège et centres de recherche Inria

Accès direct

Social