Talk "Formal Development of Multi-Purpose Interactive Application (MPIA) for ARINC 661"

by Dominique Méry

Tue, 14 January 2020 at 05:10 pm in Massa Marittima, Italy

Joint work with: Neeraj Kumar Singh, Yamine A ̈ıt Ameur Philippe Palanque, Marc Pantel

Abstract: This talks reports our experience for developing Human-MachineIn- terface (HMI) complying with ARINC 661 specification standard for interactive cockpits applications using formal methods. This development is centered around our modelling language FLUID, which is formally defined in the FORMEDI- CIS4 project. FLUID contains essential features required for specifying HMI. For developing Multi-Purpose Interactive Applications (MPIA), we follow the following steps: an abstract model of MPIA is developed in the FLUID language; the MPIA FLUID model is used to produce an Event-B model for checking the functional behaviour, user interactions, safety properties, and interaction related to domain properties; the Event-B model is also used to check temporal proper- ties and possible scenario using the ProB model checker; and finally, the MPIA FLUID model is translated to Interactive Cooperative Objects (ICO) using Pet- Shop CASE tool to validate the dynamic behaviour, visual properties and task analysis. These steps rely on different tools to check internal consistency along with possible HMI properties. Finally, the formal development of MPIA case study using FLUID and diving into other formal techniques, demonstrates relia- bility, scalability and feasibility of our approach presented in the FORMEDICIS project.