DS0703 -

FORmal MEthods for the Development and the engIneering of Critical Interactive Systems – FORMEDICIS

Submission summary

FORMEDICIS is a 48months project proposedbyfive academicand industrial partners: ONERA(coordinator), IRIT/INPT,ENAC, LORIA-Université de Lorraine and Ingenuity io. An earlier version of this project was submitted to the program ANR 2015.

In the last 30 years, the aerospace domain has successfully devised rigorous methods and tools for the development of safe functionally-correct software. During this process, interactive software has received a relatively lower amount of attention. However, highly interactive Human-System Interactions (HSI) are now appearing in critical systems and especially in aeronautics: new generations of aircraft cockpits make use of sophisticated electronic devices that may be driven by more and more complex software applications.

The criticality of these applications do require a high degree of assurance for their intended behavior. For instance the report by the French BEA about the crash of the Rio-Paris flight AF 447 A330 Airbus points out a design issue in the behaviour of the Flight Director interface as one of the original causes of the crash. There is a real stake to improve the development of these critical interactive applications.

The problem is that standard processes for the development of safety critical software in aeronautics are based on a V model and are not really suitable for interactive software design for which more iterative and agile methods that involve end-users and that mix design and verifications are required. Moreover, the stakeholders that participate in the design of these applications do not have real common means to express properly and rigorously the intended behaviourof these interfaces.

We believe that part of these issues are due to the lack of a well-defined domain specific language to represent interactive software design in a way that allows system designers to iterate on their designs before injecting them in a development process and system developers to verify their software against the chosen design.

Such a hub language (similar to VHDL for hardware description, Scade for safety-critical control and command software development or more generally AADL for achitectures) will bring increased flexibility in the development process leading not only to easier iterations within and between the different phases of a V model but also to the automation of parts of the process.

FORMEDICIS aims at designing such a formal hub language, L. This language will permit the designers to express their requirements concerning the interactive behaviour that must be embedded inside the interactive applications. It will be sufficiently abstract and friendly to be used, despite their different scientific skills, by all stakeholders involved in the development process. Being domain specific, it will contain the right abstractions to deal with the specific features of the HSI domain.

FORMEDICIS will also develop a framework devoted to the validation, verification, and implementation of critical interactive applications designed and denoted in L, facing various scientific and technological challenges:
- Designing adequate formalized transformation rules from the L language to verification tools for proving or checking properties on these models;
- Designing concretization rules and adequate transformation rules to translate L into software compliant with ARINC 661 or with the djnn framework devoted to post-WIMP (Windows, Icons, Menus, Pointer) applications;
- Verifying these transformation rules and their results;
- Handling post-WIMP interfaces;
- Contributing to the certification progress.

Developments will be released as free open source software. To address future industrial systems, we insist on providing convincing proof of concepts for our ideas to hopefully lead to subsequent industrial research projects and fuel safety critical development standards, and then addressing other domains such as automotive, railway, factory automation, nuclear power or healthcare.

Project coordinator

Monsieur David CHEMOUIL (ONERA CENTRE PALAISEAU)

The author of this summary is the project coordinator, who is responsible for the content of this summary. The ANR declines any responsibility as for its contents.

Partner

LORIA Laboratoire Lorrain de Recherche en Informatique er ses Applications
INGENUITY I/O
ONERA CENTRE PALAISEAU
IRIT/INPT
ENAC Ecole Nationale de l'Aviation Civile

Help of the ANR 943,337 euros
Beginning and duration of the scientific project: January 2017 - 48 Months

Useful links