基于HOL4的形式化方法
DOI:
作者:
作者单位:

作者简介:

通讯作者:

基金项目:

国家自然科学基金(61373034)


Formal Method Based on HOL4
Author:
Affiliation:

Fund Project:

  • 摘要
  • |
  • 图/表
  • |
  • 访问统计
  • |
  • 参考文献
  • |
  • 相似文献
  • |
  • 引证文献
  • |
  • 资源附件
    摘要:

    针对计算机系统设计的正确性问题,研究了一种在测试空间上完备的形式化方法,探讨了硬件系统在定理证明器HOL4中进行形式化验证的一般方法,其中包括如何采用高阶逻辑形式化描述系统的实现与规范,以及在HOL4中证明目标的一般过程.同时,以乘法器为实例,提出一种功能分解法对需要分析的电路进行形式化建模,并对模型的性质在HOL4中进行推理与验证,从而证明了乘法器电路设计的模型满足所提取的性质.

    Abstract:

    In order to solve the correctness issues of computer system design, a formal method which is complete on the test space is studied a general method of formal verification of hardware system in HOL4 is discussed in this paper. The method includes how to use the higher-order logic to describe the implementation and specification of hardware system and the general process of proving goals in HOL4. Meanwhile, taking multiplier as example, a functional decomposition method for modeling the design of circuit logically is proposed. Relevant properties of the circuit are ratiocinated and verified using the theorem prover HOL4, which proves that the model of the circuit design satisfies the properties.

    参考文献
    相似文献
    引证文献
引用本文

张杰,饶文博,王少超,李晓娟.基于HOL4的形式化方法.计算机系统应用,2016,25(2):202-207

复制
分享
文章指标
  • 点击次数:
  • 下载次数:
历史
  • 收稿日期:2015-05-12
  • 最后修改日期:2015-06-03
  • 录用日期:
  • 在线发布日期: 2016-02-23
您是第位访问者
版权所有:中国科学院软件研究所 京ICP备05046678号-3
地址:北京海淀区中关村南四街4号 中科院软件园区 7号楼305房间,邮政编码:100190
电话:010-62661041 传真: Email:csa (a) iscas.ac.cn
技术支持:北京勤云科技发展有限公司

京公网安备 11040202500063号