A Framework for Critical Interactive System Formal Modelling and Analysis

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.