OATAO - Open Archive Toulouse Archive Ouverte Open Access Week

Certified embedding of B models in an integrated verification framework

Halchin, Alexandra and Aït-Ameur, Yamine and Singh, Neeraj Kumar and Feliachi, Abderrahmane and Ordioni, Julien Certified embedding of B models in an integrated verification framework. (2019) In: 13th International Symposium on Theoretical Aspects of Software Engineering (TASE 2019), 29 July 2019 - 31 July 2019 (Guilin, China).

(Document in English)

PDF (Author's version) - Requires a PDF viewer such as GSview, Xpdf or Adobe Acrobat Reader

Official URL: https://doi.org/10.1109/TASE.2019.000-4


To check the correctness of heterogeneous models of a complex critical system is challenging to meet the certification standard. Such guarantee can be provided by embedding the heterogeneous models into an integrated modelling framework. This work is proposed in the B-PERFect project of RATP (Parisian Public Transport Operator and Maintainer), it aims to apply formal verification using the PERF approach on the integrated safety-critical software related to railway domain expressed in a single modelling language: HLL. This paper presents a certified translation from B formal language to HLL. The proposed approach uses HOL as a unified logical framework to describe the formal semantics and to formalize the translation relation of both languages. The developed Isabelle/HOL models are proved in order to guarantee the correctness of our translation process. Moreover, we have also used weak-bisimulation relation to check the correctness of translation steps. The overall approach is illustrated through a case study issued from a railway software system: onboard localization function. Furthermore, it discusses the integrated verification at the system level.

Item Type:Conference or Workshop Item (Paper)
Additional Information:Thanks to the IEEE (Institute of Electrical and Electronics Engineers). This paper is available at : https://ieeexplore.ieee.org/document/8914050 “© 2019 IEEE. Personal use of this material is permitted. Permission from IEEE must be obtained for all other uses, in any current or future media, including reprinting/republishing this material for advertising or promotional purposes, creating new collective works, for resale or redistribution to servers or lists, or reuse of any copyrighted component of this work in other works.
HAL Id:hal-02421919
Audience (conference):International conference proceedings
Uncontrolled Keywords:
Institution:French research institutions > Centre National de la Recherche Scientifique - CNRS (FRANCE)
Université de Toulouse > Institut National Polytechnique de Toulouse - Toulouse INP (FRANCE)
Université de Toulouse > Université Toulouse III - Paul Sabatier - UT3 (FRANCE)
Université de Toulouse > Université Toulouse - Jean Jaurès - UT2J (FRANCE)
Université de Toulouse > Université Toulouse 1 Capitole - UT1 (FRANCE)
Other partners > Régie Autonome des Transports Parisiens - RATP (FRANCE)
Laboratory name:
Deposited On:20 Dec 2019 16:14

Repository Staff Only: item control page