International audience

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.

Abstract This paper presents a formal development approach for designing interactive applications using a correct-by-construction approach. In this work, we propose a refinement strategy using model-view-controller (MVC) to structure and design Event-B formal models of the interactive application. The proposed MVC-based refinement strategy facilitates the development of an abstract model and a series of refined models by introducing the possible modes, controller’s behaviour and visual components of the interactive application while preserving the required interaction-related safety properties. To demonstrate the effectiveness, scalability, reliability and feasibility of our approach, we use a small example (from automotive domain) and real-life industrial case studies (from aviation). The entire development is realized in Event-B and the associated Rodin tool is used to analyse and verify the correctness of the formalized model. Finally, the developed Event-B models are used to generate source code using EB2ALL tool for going from the specification to the implementation of the interactive application.

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.

Refactoring, successfully used in the field of programming, can be used in maintenance and restructuring of the large and complex models. In this paper, we present a novel approach for model refactoring and a set of modelling patterns that are applicable for refinement-based formal development. In order to carry out this study, we investigate the previously developed large and complex model and required ontology to develop a domain model and a refactored system model. Further, we use the Rodin tools to check the internal consistency with respect to the desired functional behaviour and the required safety properties. Our main contributions are: to develop a refactoring technique related to the correct by construction approach; to use the domain specific knowledge in a system model explicitly; to define a set of modelling patterns; and to define a restructuring mechanism in the formal development. Finally, this proposed approach is evaluated through a complex medical case study: ECG clinical assessment protocol.

Dynamic networks are characterized by frequent topology changes due to the unpredictable appearance and disappearance of mobile devices and/or communication links. In this paper, we propose a correct-by-construction approach for proving distributed algorithms in a forest of spanning trees. Our approach consists in two phases. The first one aims to control the dynamic structure of the network by triggering a maintenance operation when the forest is altered. To do so, we develop a formal pattern using the Event-B method which is based on an existing model for building and maintaining a spanning forest in dynamic networks. The second phase of our approach deals with distributed algorithms which can be applied to spanning trees. We illustrate our pattern through an example of a leader election algorithm. The proof statistics show that our solution can save efforts on specifying as well as proving the correctness of distributed algorithms in a forest of spanning trees.

Formal methods have emerged as an alternative approach to ensuring quality and correctness of highly critical systems, overcoming limitations of traditional validation techniques such as simulation and testing. We propose a refinement-based methodology for complex medical systems design, which possesses all the required key features. A refinement-based combined approach of formal verification, model validation using a model-checker and refinement chart is proposed in this methodology for designing a high-confidence medical device. Furthermore, we show the effectiveness of this methodology for the design of a cardiac pacemaker system.

The snapshot problem addresses a collection of important algorithmic issues related to the distributed computations, which are used for debugging or recovering the distributed programs. Among the existing solutions, Chandy and Lamport propose a simple distributed algorithm. In this paper, we explore the correct-by-construction process to formalize the snapshot algorithms in distributed system. The formalization process is based on a modeling language Event B, which supports a refinement-based incremental development using RODIN platform. These refinement-based techniques help to derive a correct distributed algorithm. Moreover, we demonstrate how this class of other distributed algorithms can be revisited. A consequence is to provide a fully mechanized proof of the distributed algorithms.

The storage of votes is a critical component of any voting system. In traditional systems there is a high level of transparency in the mechanisms used to store votes, and thus a reasonable degree of trustworthiness in the security of the votes in storage. This degree of transparency is much more difficult to attain in electronic voting systems, and so the specific mechanisms put in place to ensure the security of stored votes require much stronger verification in order for them to be trusted by the public. There are many desirable properties that one could reasonably expect a vote store to exhibit. From the point of view of security, we argue that tamper-evident storage is one of the most important requirements: the changing, or deletion of already validated and stored votes should be detectable; as should the addition of unauthorised votes after the election is concluded. We propose the application of formal methods (in this paper, event- B) for guaranteeing, through construction, the correctness of a vote store with respect to the requirement for tamper- evident storage. We illustrate the utility of our refinement- based approach by verifying - through the application of a reusable formal design pattern - a store design that uses a specific PROM technology and applies a specific encoding mechanism.

Abstract. The IEEE 1394 tree identify protocol illustrates the adequacy of the event-driven approach used together with the B Method. This approach provides a complete framework for developing mathematical models of distributed algorithms. A specific development is made of a series of more and more refined models. Each model is made of a number of static properties (the invariant) and dynamic parts (the guarded events). The internal consistency of each model as well as its correctness with regard to its previous abstraction are proved with the proof engine of Atelier B, which is the tool associated with B. In the case of IEEE 1394 tree identify protocol, the initial model is very primitive: it provides the basic properties of the graph (symmetry, acyclicity, connectivity), and its dynamic parts essentially contain a single event which elects the leader in one shot. Further refinements introduce more events, showing how each node of the graph non-deterministically participates in the leader election. At some stage in the development, message passing is introduced. This raises a specific potential contention problem, whose solution is given. The last stage of the refinement completely localises the events by making them take decisions based on local data only.

This paper presents the specification of telecommunication services using B abstract machines, and it defines the feature interaction problem as an interference issue among processes sharing common resources. The work reported is experimental in nature as we explore the way in which to use the B method to tackle the feature interaction problem in telecommunication services. The B method is a tool for specifying, refining and developing systems in a mathematical and rigorous, but simple, way. Services are specified using the B method and the feature interaction problem is modelled as a violation of invariant properties. The B method is supported by software that helps the specifier of services and features. We have not only modelled services within the B technology, but we have also extended the B methodology with a novel way of combining abstract machines.