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

FORMEDICIS attaque cette question via la mise au point de FLUID, un langage dédié à ce domaine, ainsi
que de méthodes et outils formels associés.
Le langage permet aux concepteurs de décrire le comportement interactif embarqué au sein des applications
et attendu d’elles. Ce comportement est décrit au moyen d’une machine à états. Le langage permet de tenir
compte explicitement de l’environnement et des hypothèses sur le domaine d’application. Il offre aussi diverses
facilités pour décrire les propriétés attendues de l’application, en particulier inspirées de notations communes
dans cette discipline.

Un modèle FLUID peut alors faire l’objet d’une validation par model-checking via une transformation vers
l’outil Alloy 6. Passée la validation, un développement formel basé sur le raffinement peut être effectué au
moyen de la méthode Event-B. De plus, un modèle d’objets coopératifs interactifs (ICO) est dérivé du modèle
Event-B pour l’animation, la visualisation et la validation des comportements dynamiques, des propriétés visuelles et de l’analyse des tâches. Enfin, nous avons proposé une traduction du langage FLUID vers le langage
Smala (un langage réactif pour le développement d’applications interactives).
Le projet a mis en évidence une approche permettant de développer formellement des systèmes interactifs
critiques. L’approche se fonde sur un langage pivot intégrant en particulier des constructions pour l’annotation
de modèles (tags) et la prise en compte de l’environnement. Des techniques de validation, vérification, raffinement et génération de code sont mises en œuvre. Les ponts entre les diverses méthodes formelles et le langage
pivot FLUID ont été réalisés offrant, de plus, des contributions positionnant les notations et langages sur le
cycle de développement des systèmes interactifs. Ces diverses contributions ont été appliquées sur plusieurs
cas d’étude.

En termes de perspectives, l’étude pourrait se poursuivre par une meilleure prise en compte de l’utilisateur.
Un autre axe de poursuite concernerait la prise en compte d’interfaces innovantes qui sont plus particulièrement
étudiées dans le domaine de l’Interaction Homme-Machine. Enfin, les applications et cas d’études exploités
dans FORMEDICIS restent relativement simples et ont été étudiés en dehors de leur contexte opérationnel. Une
perspective très intéressante serait de confronter les différentes contributions (notations, outils, processus) à
des cas industriels pour identifier des pistes d’amélioration.

La production scientifique concerne d’une part des communications sur les méthodes utilisées, étendues
ou développées dans le projet (plus de 20 articles dans des revues et conférences internationales), et d’autre
part la production de prototypes logiciels et de modèles formels.

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é.