Geniet, Romain and Singh, Neeraj Kumar
Refinement Based Formal Development of Human-Machine Interface.
(2018)
In: 7th International Workshop on Formal Methods for Interactive Systems (FMIS), 25 June 2018 (Toulouse, France).
|
(Document in English)
PDF (Author's version) - Requires a PDF viewer such as GSview, Xpdf or Adobe Acrobat Reader 759kB |
Official URL: https://doi.org/10.1007/978-3-030-04771-9_19
Abstract
Human factors have been considered as the most common causes of accidents, particularly for interacting with complex critical systems related to avionics, railway, nuclear and medical domains. Mostly, a human-machine in- terface (HMI) is developed independently and the correctness of possible inter- actions is heavily dependent on testing, which cannot guarantee the absence of run-time errors. The use of formal methods in HMI development may assure such guarantee. This paper presents a methodology for developing an HMI using a correct by construction approach, which allows us to introduce the HMI components, functional behaviour and the required safety properties progressively. The proposed methodology, generic refinement strategy, supports the development of the model-view-controller (MVC) architecture. The whole approach is formalized using Event-B and relies on the Rodin tools to check the internal consistency with respect to the given safety properties, invariants and events. Finally, an industrial case study is used to illustrate the effectiveness of our proposed approach for developing an HMI.
Item Type: | Conference or Workshop Item (Paper) |
---|---|
HAL Id: | hal-02353335 |
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 Rennes 1 (FRANCE) |
Laboratory name: | |
Statistics: | download |
Deposited On: | 07 Nov 2019 10:45 |
Repository Staff Only: item control page