Certified Embedding of B Models in an Integrated Verification Framework
Certified Embedding of B Models in an Integrated Verification Framework
复制标题
B 模型在集成验证框架中的嵌入认证
DOI：
--
复制
发表时间：
2019
期刊：
影响因子：
--
通讯作者：
J. Ordioni
中科院分区：
文献类型：
--
作者：
Alexandra Halchin;Y. A. Ameur;N. Singh;Abderrahmane Feliachi;J. Ordioni
复杂关键系统的异构模型的正确性检查是一个挑战，以满足认证标准。这种保证可以通过将异构模型嵌入到集成建模框架中来提供。这项工作是在RATP（巴黎公共交通运营商和维护商）的B-PERFect项目中提出的，它旨在使用PERF方法对以单一建模语言HLL表示的与铁路领域相关的集成安全关键软件进行形式化验证。本文提出了一种从B形式语言到HLL的认证翻译。该方法使用HOL作为一个统一的逻辑框架来描述形式语义和形式化的两种语言的翻译关系。为了保证翻译过程的正确性，对所开发的Isabelle/HOL模型进行了证明。此外，我们还使用弱互模拟关系来检查翻译步骤的正确性。通过一个铁路软件系统：车载定位功能的案例研究，说明了整体方法。此外，还讨论了系统级的集成验证。
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 system level.