L'Agence nationale de la recherche Des projets pour la science

Translate this page in english

(DS0703) 2016
Projet FORMEDICIS

Méthodes formelles pour le développement et l'ingénierie de systèmes interactifs critiques

FORMEDICIS est un projet de 48 mois soumis par cinq partenaires académiques et industriels : l'ONERA (coordinateur), IRIT/INPT, l'ENAC, le LORIA-Université de Lorraine et Intactile Ingenuity. Une version antérieure de ce projet a été soumise dans le cadre du programme ANR 2015.

Le domaine aérospatial a vu l'émergence de méthodes et d'outils rigoureux pour le développement de logiciels sûrs et corrects d'un point de vue fonctionnel. Les logiciels interactifs n'ont pas bénéficié de la même attention. Or les systèmes critiques, particulièrement aéronautiques, ont embarqué de nouveaux dispositifs hautement interactifs : les cockpits de nouvelle génération font appel une électronique sophistiquée pilotée par des applications logicielles complexes.

Leur criticité exige de ces applications un haut niveau d'assurance sur le comportement attendu d'elles. Le rapport du BEA concernant le crash de l'Airbus A330 AF447 identifie le comportement défectueux de l'interface du directeur de vol comme la source des fautes ayant conduit au crash de l'avion. La maîtrise de ces logiciels interactifs critiques constitue donc un enjeu bien réel.

Le problème est que les approches suivies pour le développement des logiciels critiques sûrs, dans le domaine aéronautique, se fondent sur des cycles de développements en V incompatibles avec les exigences du logiciel d'interaction requérant des méthodes plus itératives et agiles impliquant les usagers en alternant phases de conception et de test. Et l'ensemble très divers des participants à la conception de ces applications ne partage aucun moyens communs favorisant l'expression précise du comportement attendu de ces interfaces.

Nous pensons qu'une part importante de ces difficultés est imputable au manque d'un langage bien défini, spécifique au domaine, permettant, par le biais de leur représentation partagée, aux concepteurs de ces applications d'itérer sur leurs conceptions avant de les soumettre au développement et aux développeurs de vérifier que leur produit est conforme à une spécification de référence.

Un tel langage apportera une plus grande flexibilité dans le processus de développement en facilitant les itérations entre ses différentes phases mais également en permettant l'automatisation de certaines d'entre elles.

FORMEDICIS définira ce langage L. Il permettra aux concepteurs de décrire le comportement interactif embarqué au sein des applications et attendu d'elles. Suffisamment abstrait et convivial, il sera accessible, par delà leurs compétences scientifiques très différentes, à tous les participants au développement de ces logiciels. Lui étant spécifique et dédié, il offrira les abstractions du domaine de l'interaction homme système.

FORMEDICIS propose un environnement dévolu à la vérification, la validation et l'implantation d'applications interactives critiques décrites en L. A cet effet plusieurs verrous devront être levés :
- définir des règles de transformations permettant de modéliser des descriptions L afin de vérifier ou prouver des propriétés sur ces modèles ;
- définir des règles de concrétisation et des transformations de L afin de le compiler dans du code compatible ARINC 661 ou ciblant l'environnement djnn dévolu aux applications post-WIMP ;
- vérifier la correction des règles ainsi que leurs résultats ;
- traiter des interfaces post-WIMP;
- contribuer au progrès des processus de certification.

Ces développements seront réalisés en libre. Voulant contribuer au développement de futurs sytèmes industriels nous chercherons à apporter tout au long du projet une démonstration convaincante d'idées pouvant conduire à de nouveaux projets de recherche industriels et à participer à l'évolution des standards de développement de systèmes critiques, en envisageant de cibler de nouveaux domaines applicatifs comme ceux de l'automobile, du rail, du nucléaire ou de la santé.

Partenaires

ENAC Ecole Nationale de l'Aviation Civile

 INGENUITY I/O

 IRIT/INPT

LORIA Laboratoire Lorrain de Recherche en Informatique er ses Applications

 ONERA CENTRE PALAISEAU

Aide de l'ANR 943 337 euros
Début et durée du projet scientifique janvier 2017 - 48 mois

 

Programme ANR : (DS0703) 2016

Référence projet : ANR-16-CE25-0007

Coordinateur du projet :
Monsieur Bruno d'Ausbourg (ONERA CENTRE PALAISEAU)

 

Revenir à la page précédente

 

L'auteur de ce résumé est le coordinateur du projet, qui est responsable du contenu de ce résumé. L'ANR décline par conséquent toute responsabilité quant à son contenu.