Interactive system development does not follow the same life cycle as other system developments. The essential differences lie in the iterative nature of such system development. Throughout iterations, the requirements undergo many changes due to the evolution of customer’s needs and user feedback after experiencing prototypes. The challenge is tougher in the case of critical HCI (aircraft cockpits, medical systems, nuclear power plant etc.). Indeed, critical HCI requires to be designed and built such that safety and security requirements are thoroughly fulfilled. This paper presents a novel development framework featuring formal verification and validation of critical interactive systems at modelling level. It identifies the several challenges of the interactive system development and settles down the main objectives. Furthermore, it sketches the most important traits of the proposed approach to circumvent the enumerated challenges. Hence, we discuss the importance of the pivot language Fluid, the domain theory specific to interactive systems and their modelling using Event-B.
If you cannot see the document below, the PDF document is most likely not freely accessible. In this case, please try to access the document via this link.
% BibTex
@inproceedings{Mendil20,
author = {Isma{\"{\i}}l Mendil},
editor = {Alexander Raschke and
Dominique M{\'{e}}ry and
Frank Houdek},
title = {A Framework for Critical Interactive System Formal Modelling and Analysis},
booktitle = {Rigorous State-Based Methods - 7th International Conference, {ABZ}
2020, Ulm, Germany, May 27-29, 2020, Proceedings},
series = {Lecture Notes in Computer Science},
volume = {12071},
pages = {423--426},
publisher = {Springer},
year = {2020},
url = {https://doi.org/10.1007/978-3-030-48077-6\_36},
doi = {10.1007/978-3-030-48077-6\_36},
timestamp = {Mon, 25 May 2020 12:33:39 +0200},
biburl = {https://dblp.org/rec/conf/asm/Mendil20.bib},
bibsource = {dblp computer science bibliography, https://dblp.org}
}