Formal Development of Multi-Purpose Interactive Application (MPIA) for ARINC 661 - Assistance à la Certification d’Applications DIstribuées et Embarquées Accéder directement au contenu
Communication Dans Un Congrès Année : 2020

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

Résumé

This paper reports our experience for developing Human-Machine Interface (HMI) complying with ARINC 661 specification standard for interactive cockpits applications using formal methods. This development relies on the FLUID modelling language, we have proposed and formally defined in the FORMEDICIS project. FLUID contains essential features required for specifying HMI. To develop the Multi-Purpose Interactive Applications (MPIA) use case, we follow the following steps: an abstract model of MPIA is written using the FLUID language; this 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 properties and possible scenario using the ProB model checker; and finally, the MPIA FLUID model is translated to Interactive Cooperative Objects (ICO) using the PetShop 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 the MPIA case study using FLUID and its embedding into other formal techniques, demonstrates reliability, scalability and feasibility of our approach defined in the FORMEDICIS project.
Fichier principal
Vignette du fichier
singh_26285.pdf (782.1 Ko) Télécharger le fichier
Origine : Fichiers produits par l'(les) auteur(s)
Loading...

Dates et versions

hal-02942767 , version 1 (18-09-2020)

Identifiants

Citer

Neeraj Kumar Singh, Yamine Aït-Ameur, Dominique Méry, David Navarre, Philippe Palanque, et al.. Formal Development of Multi-Purpose Interactive Application (MPIA) for ARINC 661. 7th International Workshop on Formal Techniques for Safety-Critical Systems (FTSCS 2019), Nov 2019, Shenzhen, China. pp.21-39, ⟨10.1007/978-3-030-46902-3_2⟩. ⟨hal-02942767⟩
113 Consultations
76 Téléchargements

Altmetric

Partager

Gmail Facebook X LinkedIn More