Certified embedding of B models in an integrated verification framework

Alexandra Halchin (1) , Yamine Aït-Ameur (1, 2) , Neeraj Kumar Singh (1, 2) , Abderrahmane Feliachi (3) , Julien Ordioni (3)

1 IRIT-ACADIE - Assistance à la Certification d’Applications DIstribuées et Embarquées
2 Toulouse INP - Institut National Polytechnique (Toulouse)
3 RATP - Régie Autonome des Transports Parisiens

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.

Mots clés: B to HLL translation validation; Theorem proving; Model animation; Formal semantics

Domaines: Autre [cs.OH]

Alexandra Halchin, Yamine Aït-Ameur, Neeraj Kumar Singh, Abderrahmane Feliachi, Julien Ordioni. Certified embedding of B models in an integrated verification framework. 2019 International Symposium on Theoretical Aspects of Software Engineering (TASE), Jul 2019, Guilin, China. pp.168-175. ⟨hal-02421919⟩