Skip to Main content Skip to Navigation
Conference papers

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

Abstract : 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.
Complete list of metadatas

Cited literature [30 references]  Display  Hide  Download
Contributor : Open Archive Toulouse Archive Ouverte (oatao) <>
Submitted on : Friday, September 18, 2020 - 11:41:56 AM
Last modification on : Thursday, September 24, 2020 - 3:34:03 AM


Files produced by the author(s)



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⟩



Record views


Files downloads