Affordable Access

An Integrated Framework for the Formal Analysis of Critical Interactive Systems

  • Mendil, Ismaël
  • Singh, Neeraj Kumar
  • Aït-Ameur, Yamine
  • Méry, Dominique
  • Palanque, Philippe
Publication Date
Dec 01, 2020
External links


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.

Report this publication


Seen <100 times