Skip to Main content Skip to Navigation
New interface
Conference papers

An Integrated Framework for the Formal Analysis of Critical Interactive Systems

Ismaël Mendil 1 Neeraj Kumar Singh 1, 2 Yamine Aït-Ameur 1, 2 Dominique Méry 3, 4, 5, 6 Philippe Palanque 7 
3 VERIDIS - Modeling and Verification of Distributed Algorithms and Systems
MPII - Max-Planck-Institut für Informatik, Inria Nancy - Grand Est, LORIA - FM - Department of Formal Methods
6 MOSEL - Proof-oriented development of computer-based systems
LORIA - FM - Department of Formal Methods
7 IRIT-ICS - Interactive Critical Systems
IRIT - Institut de recherche en informatique de Toulouse
Abstract : When interactive systems allow users to interact with critical systems, they are qualified as Critical Interactive Systems, CIS for short. Their design requires the support of different activities and tasks to achieve user goals. Examples of such systems are cockpits, nuclear plant control panels, medical devices, etc. Such critical systems are very difficult to model due to the complexity of the offered interaction capabilities. %humans in the loop.%This paper presents a formal framework, F3FLUID (Formal Framework For FLUID), for designing safety-critical interactive systems. It relies on FLUID as core modelling language. FLUID enables the modelling and use of interactive systems domain concepts and supports an incremental design of such systems. Formal verification, validation and animation of the designed models are supported through different transformations of FLUID models into target formal verification techniques: %to analyse consistency by transformation for FLUID models. Event-B for formal verification, ProB model checker for animation and Interactive Cooperative Objects for user validation. The Event-B models are generated from FLUID while ICO and ProB models are produced from Event-B. We exemplify the real-life case study TCAS (Traffic alert and Collision Avoidance System) to demonstrate our framework.
Complete list of metadata
Contributor : Dominique Méry Connect in order to contact the contributor
Submitted on : Tuesday, November 10, 2020 - 5:57:04 PM
Last modification on : Monday, July 4, 2022 - 8:50:11 AM


  • HAL Id : hal-02999148, version 1


Ismaël Mendil, Neeraj Kumar Singh, Yamine Aït-Ameur, Dominique Méry, Philippe Palanque. An Integrated Framework for the Formal Analysis of Critical Interactive Systems. The 27th Asia-Pacific Software Engineering Conference, Jun Sun, Dec 2020, Singapour, Singapore. pp.10. ⟨hal-02999148⟩



Record views