Abstract This paper proposes a unified formal framework, Formal Framework For FLUID (F3FLUID), for the development of safety‐critical interactive systems. This framework is based on the Formal Language of User Interface Design (FLUID) pivot modeling language defined in the FORMEDICIS project, which enables high‐level system requirements for interactive systems to be specified in the FLUID language. This modeling language is specifically designed for handling concepts of safety‐critical interactive systems, including domain knowledge. A FLUID model is used as a source model for the generation of several target models in different modeling languages to support the formal verification methods, such as theorem proving and model checking. In this paper, we use the Event‐B modeling language for checking functional behaviors, user interactions, safety properties, and domain properties. A FLUID model is transformed into an Event‐B model, and then, the Rodin tool is used to check the internal consistency with respect to the given safety properties. We illustrate the operational semantics of the FLUID language, and the transformation strategy of FLUID models into Event‐B models, including the tool development. We use the ProB model checker to analyze the temporal properties and to animate the formalized specification. In addition, an interactive cooperative objects (ICOs) model is derived from the Event‐B model for animation, visualization and validation of dynamic behaviors, visual properties, and task analysis. Finally, an industrial case study, complying with the ARINC 661 standard, Multi‐Purpose Interactive Applications (MPIA), is used to illustrate the effectiveness of our F3FLUID framework for the development of safety‐critical interactive systems.

System engineering advocates a thorough under-standing of the engineering domain or certification standards (aeronautics, railway, medical, etc.) associated to the system under design. In this context, engineering domain knowledge plays a predominant role in system design and/or certification. Furthermore, it is a prerequisite to achieve the effectiveness and performance of the designed system. This article proposes a formal method for describing and setting up domain-specific behavioural analyses. It defines a formal verification technique for dynamic properties entailed by engineering domain knowledge where Event-B formal models are annotated and analysed in a non-intrusive way, i.e. without destructive alteration. This method is based on the formalisation of behavioural properties analyses relying on domain knowledge as an ontology on the one hand and a meta-theory for Event-B on the other hand. The proposed method is illustrated using a critical interactive system.

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. This paper presents a formal framework, F3FLUID (Formal Framework For FLUID), for designing safety-critical interactive systems. It relies on FL UID as core modelling language. FL UID 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: 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.