Interactive systems verification and certification methods

Formedicis

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

 

Objectives

FORMEDICIS is a 48 months project proposed by five academic and industrial partners: ONERA (coordinator), IRIT/INPT, ENAC, LORIA-Université de Lorraine and Ingenuity io.

FORMEDICIS aims at designing a formal language, named Fluid . This language will permit the designers to express their requirements concerning the interactive behaviour that must be embedded inside 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 Fluid, 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.

http://www.agence-nationale-recherche.fr/projet-anr/?tx_lwmsuivibilan_pi2%5BCODE%5D=ANR-16-CE25-0007

 

Case study

Traffic alert and Collision Avoidance System

Formal verification