HAL will be down for maintenance from Friday, June 10 at 4pm through Monday, June 13 at 9am. More information
Skip to Main content Skip to Navigation
Conference papers

Standard Conformance-by-Construction with Event-B

Ismail Mendil 1 Yamine Aït-Ameur 1 Neeraj Singh 1 Dominique Méry 2, 3, 4 Philippe Palanque 5
4 VERIDIS - Modeling and Verification of Distributed Algorithms and Systems
LORIA - FM - Department of Formal Methods , Inria Nancy - Grand Est, MPII - Max-Planck-Institut für Informatik
5 IRIT-ICS - Interactive Critical Systems
IRIT - Institut de recherche en informatique de Toulouse
Abstract : Checking the conformance of a system design to a standard is a central activity in the system engineering life cycle, a fortiori when the concerned system is deemed critical. Standard conformance checking entails ensuring that a system or a model of a system faithfully meets the requirements of a specification of a standard improving the robustness and trustworthiness of the system model. In this paper, we present a formal framework based on the correct-by-construction Event-B method and related theories for formally checking the conformance of a formal system model to a formalised standard specification by construction. This framework facilitates the formalization of standard concepts and rules as an ontology, as well as the formalization of an engineering domain, using an Event-B theory consisting of data types and a collection of operators and properties. Conformance checking is accomplished by annotating the system model with typing conditions. We address an industrial case study borrowed from the aircraft cockpit engineering domain to demonstrate the feasibility and strengths of our approach. The ARINC 661 standard is formalised as an Event-B theory. This theory formally models and annotates the safety-critical real-world application of a weather radar system for certification purposes.
Complete list of metadata

Contributor : Ismail Mendil Connect in order to contact the contributor
Submitted on : Monday, August 30, 2021 - 11:35:27 AM
Last modification on : Thursday, February 10, 2022 - 2:16:02 PM


Files produced by the author(s)



Ismail Mendil, Yamine Aït-Ameur, Neeraj Singh, Dominique Méry, Philippe Palanque. Standard Conformance-by-Construction with Event-B. 26th International Conference on Formal Methods for Industrial Critical Systems (FMICS 2021), European Research Consortium for Informatics and Mathematics: ERCIM, Working Group on Formal Methods for Industrial Critical Systems, Aug 2021, Paris (virtual), France. pp.126-146, ⟨10.1007/978-3-030-85248-1_8⟩. ⟨hal-03487118v1⟩



Record views


Files downloads