Détail d'une fiche   Version PDF

FORMES (SR0340AR)

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

FORMES


Statut: Terminée

Responsable : Vania Joloboff

Mots-clés de "A - Thèmes de recherche en Sciences du numérique - 2023" : Aucun mot-clé.

Mots-clés de "B - Autres sciences et domaines d'application - 2023" : Aucun mot-clé.

Domaine : Algorithmique, programmation, logiciels et architectures
Thème : Programmation, vérification et preuves

Période : 01/01/2009 -> 31/12/2013
Dates d'évaluation :

Etablissement(s) de rattachement : <sans>
Laboratoire(s) partenaire(s) : <sans UMR>

CRI : Siège
Localisation : Institute of Automation - LIAMA
Code structure Inria : 021097-0

Numéro RNSR : 200921233V
N° de structure Inria: SR0340AR

Présentation

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.