Projet QUARTEFT

accédez à l'espace privé du projet (GForge enseeiht) (contact: F. Vernadat)

Ce projet est financé par par la FNRAE : Fondation de la Recherche pour l'Aéronautique et l'Espace

Vous pouvez retrouver une présentation des objectifs du projet Quartfet sur la fiche du projet.

Les objectifs du projet QUARTEFT reposent sur deux constats:

• la complexité croissante des systèmes embarqués critiques temps-réel conduit à exploiter des langages de modélisation les plus proches possible des spécifications du métier du concepteur. Ces langages s'adossent sur des outils de vérification de modèles permettant d’assurer la correction du système par rapport aux exigences de sûreté, performance, temps-réel, …

• les chaînes de développement de systèmes critiques basées sur ces langages de modélisation reposent le plus souvent sur des transformations entre langages, comme par exemple la génération automatique de code. Pour augmenter l'assurance que l'on peut placer dans les systèmes ainsi obtenus, ces transformations entre langages doivent être qualifiées (assurance que la transformation préserve les propriétés d’intérêts).

Pour répondre à ces constats, le projet QUARTEFT vise à développer des technologies pour faciliter les activités de modélisation, de transformation et de vérification dans le contexte des systèmes embarqués temps-réel. L’objet du projet QUARTEFT vise à développer les technologies facilitant cette approche en proposant d'une part, une extension temps réel du langage intermédiaire Fiacre, le rapprochant ainsi des langages métiers des systèmes critiques embarqués temps-réel tels que AADL et, d’autre part, de développer les techniques de construction de transformations qui facilitent la preuve de correction et le passage à l’échelle sur des modèles réels. Il s'agit donc de permettre la construction d'une chaîne correcte de transformations des langages utilisateurs vers le langage intermédiaire, puis du langage intermédiaire vers les outils de vérification actuellement disponibles tels que TINA ou CADP. L'expression des transformations et la génération des preuves associées se fera à l'aide de l'outil TOM basé sur des techniques de réécriture. L'ensemble de ces développements sera intégré dans l'outil métier Adele.

Quarteft complète les travaux précédemment réalisés dans le cadre des projets COTRE, TOPCASED, SPICES, GENEAUTO pour assurer la construction de nouvelles générations d’ateliers de développement de systèmes critiques temps-réel basées sur la vérification formelle et les langages dédiés. Les méthodes et outils issus du projet QUARTEFT seront intégrés au sein du processus et de la plate-forme de développement de calculateurs embarqués Airbus (activités produit, électronique et logiciel), issus du projet TOPCASED, de manière à être mis en œuvre opérationnellement sur les futurs programme avion.

• Kick-off meeting : 2-3 avril 2009, à Toulouse
• 2ème réunion : 29-30 septembre 2009, à Brest
• 3ème réunion : 2-3 février 2010, à Toulouse
• 4ème réunion : 1-2 juin 2010, à Nancy
• 5ème réunion : 8-9-10 novembre 2010, à Toulouse
• 6ème réunion : 22-23 février 2011, à Toulouse
• 7ème réunion : 30-31 mai 2011, à Nancy
• 8ème réunion : 27-28 septembre 2011, à Toulouse

• LAAS-CNRS
  • Bernard Berthomieu
  • Didier Le Botlan
  • Silvano Dal Zilio
  • Pierre-Emmanuel Hladik
  • Francois Vernadat
• IRIT
  • Jean-Paul Bodeveix
  • Mamoun Filali
  • Marc Pantel
  • Jean-François Rolland
• ONERA-DTIM
  • David Doose
  • Pierre Michel
• INRIA Nancy - Grand Est
  • Jean-Christophe Bach
  • Horatiu Cirstea
  • Pierre-Etienne Moreau
• AIRBUS France
  • Patrick Farail
  • Pierre Gaufillet
  • Marie-Line Valentin
• Ellidiss
  • Pierre Dissaux
  • Arnaud Schach

• Tâche 0 : Gestion scientifique, Dissémination, Coordination avec autres projets
• Tâche 1 : Spécification des besoins et Coordination des développements
• Tâche 2 : Le langage pivot RT-FIACRE
• Tâche 3 : Transformations correctes par construction
• Tâche 4 : Intégration des solutions technologiques
• Tâche 5 : Validation de l’approche proposée