OATAO - Open Archive Toulouse Archive Ouverte Open Access Week

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

Singh, Neeraj Kumar and Aït-Ameur, Yamine and Méry, Dominique and Navarre, David and Palanque, Philippe and Pantel, Marc Formal Development of Multi-Purpose Interactive Application (MPIA) for ARINC 661. (2020) In: 7th International Workshop on Formal Techniques for Safety-Critical Systems (FTSCS 2019), 9 November 2019 - 9 November 2019 (Shenzhen, China).

(Document in English)

PDF (Author's version) - Requires a PDF viewer such as GSview, Xpdf or Adobe Acrobat Reader

Official URL: https://doi.org/10.1007/978-3-030-46902-3_2


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.

Item Type:Conference or Workshop Item (Paper)
Additional Information:Thanks to Springer editor. This papers appears in Volume 1165 of CCIS: Communications in Computer and Information Science book series ISSN: 1865-0929 ISBN 978-3-030-46901-6 The original PDF is available at: https://link.springer.com/chapter/10.1007/978-3-030-46902-3_2
HAL Id:hal-02942767
Audience (conference):International conference proceedings
Uncontrolled Keywords:
Institution:French research institutions > Centre National de la Recherche Scientifique - CNRS (FRANCE)
Université de Toulouse > Institut National Polytechnique de Toulouse - Toulouse INP (FRANCE)
Université de Toulouse > Université Toulouse III - Paul Sabatier - UT3 (FRANCE)
Université de Toulouse > Université Toulouse - Jean Jaurès - UT2J (FRANCE)
Université de Toulouse > Université Toulouse 1 Capitole - UT1 (FRANCE)
Other partners > Université de Lorraine (FRANCE)
Laboratory name:
ANR : Agence Nationale de la Recherche (France) - FORMEDICIS : FORmal MEthods for the Development and the engineering of Critical Interactive Systems
Deposited On:25 Aug 2020 09:26

Repository Staff Only: item control page