...
  • 主题
高级搜索  >
历史搜索 清空历史
首页> 外文期刊>Journal of electrical and computer engineering >A Formal Verification Methodology for DDD Mode Pacemaker Control Programs
【24h】

A Formal Verification Methodology for DDD Mode Pacemaker Control Programs

机译：DDD模式起搏器控制程序的形式验证方法

获取原文
获取原文并翻译 | 示例
           
页面导航
  • 摘要
  • 著录项
  • 相似文献
  • 相关主题

摘要

Pacemakers are safety-critical devices whose faulty behaviors can cause harm or even death. Often these faulty behaviors are caused due to bugs in programs used for digital control of pacemakers. We present a formal verification methodology that can be used to check the correctness of object code programs that implement the safety-critical control functions of DDD mode pacemakers. Our methodology is based on the theory of Weil-Founded Equivalence Bisimulation (WEB) refinement, where both formal specifications and implementation are treated as transition systems. We develop a simple and general formal specification for DDD mode pacemakers. We also develop correctness proof obligations that can be applied to validate object code programs used for pacemaker control. Using our methodology, we were able to verify a control program with millions of transitions against the simple specification with only 10 transitions. Our method also found several bugs during the verification process.
机译：起搏器是对安全至关重要的设备，其错误行为会导致伤害甚至死亡。通常，这些错误行为是由于用于起搏器数字控制的程序中的错误引起的。我们提供了一种正式的验证方法，可用于检查实现DDD模式起搏器的安全关键控制功能的目标代码程序的正确性。我们的方法基于基于Weil建立的等效双仿真（WEB）改进的理论，其中正式规范和实施都被视为过渡系统。我们为DDD模式起搏器开发了一个简单而通用的正式规范。我们还制定了正确性证明义务，这些义务可用于验证用于起搏器控制的目标代码程序。使用我们的方法，我们能够对照只有10个转换的简单规范来验证具有数百万个转换的控制程序。我们的方法还在验证过程中发现了几个错误。

著录项

  • 来源
    《Journal of electrical and computer engineering》 |2015年第2015期|939028.1-939028.10|共10页
  • 作者

    Sana Shuja; Sudarshan K. Srinivasan; Shaista Jabeen; Dharmakeerthi Nawarathna;

  • 作者单位

    Department of Electrical and Computer Engineering, North Dakota State University, 1411 Centennial Boulevard, Fargo, ND 58102, USA;

    Department of Electrical and Computer Engineering, North Dakota State University, 1411 Centennial Boulevard, Fargo, ND 58102, USA;

    Department of Electrical and Computer Engineering, North Dakota State University, 1411 Centennial Boulevard, Fargo, ND 58102, USA;

    Department of Electrical and Computer Engineering, North Dakota State University, 1411 Centennial Boulevard, Fargo, ND 58102, USA;

  • 收录信息
  • 原文格式 PDF
  • 正文语种 eng
  • 中图分类
  • 关键词

相似文献

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

客服邮箱：kefu@zhangqiaokeyan.com

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

  • 客服微信

  • 服务号