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

FORMEDICIS addresses this question via the development of FLUID, a language dedicated to this field, as
well as associated formal methods and tools.
The language allows designers to describe the interactive behavior embedded within applications and expected from them. This behavior is described by means of a state machine. The language makes it possible to
explicitly take into account the environment and the assumptions on the domain of application. It also offers
various facilities for describing the expected properties of the application, in particular inspired by common
notations in this discipline.

A FLUID model can then be validated by model-checking via a transformation to the Alloy 6 tool. After
validation, formal refinement-based development can be performed using the Event-B method. Additionally,
an interactive cooperative object (ICO) model is derived from the Event-B model for animation, visualization,
and validation of dynamic behaviors, visual properties, and task analysis. Finally, we proposed a translation
from the FLUID language to the Smala language (a reactive language for the development of interactive applications).
The project demonstrated an approach for developing formally critical interactive systems. The approach
is based on a pivot language integrating in particular constructs for annotating models (tags) and accounting
for the environment. Validation techniques, verification, refinement and code generation are implemented. The
bridges between the various formal methods and the FLUID pivot language have been specified. These various
contributions have been applied to several case studies.

In terms of prospects, the study could continue with a better consideration of the user. Another axis of
research would concern the consideration of innovative interfaces which are particularly studied in the field of
Human-Computer Interaction. Finally, applications and cases of studies used in FORMEDICIS remain relatively
simple and have been studied outside of their operational context. A very interesting prospect would be to
confront the different contributions (evaluations, tools, processes) to industrial case studies to identify areas
for improvement.

On the scientific side, more than 20 articles in journals and conferences international have been published,
together with the production of prototypes software and formal models.

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.