• 主题
高级搜索  >
历史搜索 清空历史
首页> 外文会议>International conference on reliability, safety, and security of railway systems >B-PERFect Applying the PERF Approach to B Based System Developments
【24h】

B-PERFect Applying the PERF Approach to B Based System Developments

机译：B-PERFect将PERF方法应用于基于B的系统开发

获取原文
页面导航
  • 摘要
  • 著录项
  • 相似文献
  • 相关主题

摘要

An independent safety assessment of railway software systems is performed by RATP (Regie Autonome des Transports Parisiens) for all safety-critical systems before their deployment in its network. Whenever possible, this activity is performed using the PERF approach (Proof Executed over a Retro-engineered Formal model). PERF is a methodology which handles formal verification of already developed software. This approach is applied to a variety of software systems, developed using languages such as SCADE, Ada or C. It provides an alternative verification that can be applied for the independent safety assessment of critical systems used by RATP. In this paper, we propose the B-PERFect method to generalize the application of the PERF approach for critical systems which are based on the B method. In particular, this paper focuses on transformation strategy from B language to the pivot language of PERF: HLL. HLL is a synchronous data-flow language equipped with formal verification techniques. The differences between B and HLL are pointed out and the translation process is presented in this regard.
机译：铁路软件系统的独立安全评估是由RATP（巴黎瑞吉汽车运输巴黎公司）针对所有安全关键系统进行的，然后再将其部署到其网络中。只要有可能，就使用PERF方法（在经过改造的正式模型上执行的证明）执行此活动。 PERF是一种处理已开发软件的形式验证的方法。此方法适用于使用诸如SCADE，Ada或C之类的语言开发的各种软件系统。它提供了一种替代验证，可以应用于RATP所使用的关键系统的独立安全性评估。在本文中，我们提出了B-PERFect方法来概括PERF方法在基于B方法的关键系统中的应用。特别是，本文重点介绍了从B语言到PERF的主要语言HLL的转换策略。 HLL是一种配有形式验证技术的同步数据流语言。指出了B和HLL之间的差异，并就此提出了翻译过程。

著录项

相似文献

  • 外文文献
  • 中文文献
  • 专利
获取原文

客服邮箱：kefu@zhangqiaokeyan.com

京公网安备：11010802029741号 ICP备案号：京ICP备15016152号-6 六维联合信息科技 (北京) 有限公司©版权所有

  • 客服微信

  • 服务号