Accueil

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

Langages intermédiaires et technologies de transformations qualifiables pour le développement de systèmes temps-réel

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

Contexte du projet

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 ouCADP. 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 COTRETOPCASEDSPICESGENEAUTO 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.

Evénements

Participants

Description du projet

  • 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
Ċ
Pierre-Etienne Moreau,
4 déc. 2013 à 02:18