| 基于HOL4的形式化方法 |
| |
| 引用本文： | 张杰,饶文博,王少超,李晓娟.基于HOL4的形式化方法[J].计算机系统应用,2016,25(2):202-207. |
| |
| 作者姓名： | 张杰 饶文博 王少超 李晓娟 |
| |
| 作者单位： | 北京化工大学 信息科学与技术学院, 北京 100029,北京化工大学 信息科学与技术学院, 北京 100029,北京化工大学 信息科学与技术学院, 北京 100029,首都师范大学, 北京 100029 |
| |
| 基金项目： | 国家自然科学基金(61373034) |
| |
| 摘 要： | 针对计算机系统设计的正确性问题,研究了一种在测试空间上完备的形式化方法,探讨了硬件系统在定理证明器HOL4中进行形式化验证的一般方法,其中包括如何采用高阶逻辑形式化描述系统的实现与规范,以及在HOL4中证明目标的一般过程.同时,以乘法器为实例,提出一种功能分解法对需要分析的电路进行形式化建模,并对模型的性质在HOL4中进行推理与验证,从而证明了乘法器电路设计的模型满足所提取的性质.
|
| 关 键 词： | 定理证明 形式化方法 高阶逻辑 乘法器 HOL4 形式化建模 |
| 收稿时间： | 2015/5/12 0:00:00 |
| 修稿时间： | 6/3/2015 12:00:00 AM |
Formal Method Based on HOL4 |
| |
| ZHANG Jie,RAO Wen-Bo,WANG Shao-Chao and LI Xiao-Juan.Formal Method Based on HOL4[J].Computer Systems& Applications,2016,25(2):202-207. |
| |
| Authors: | ZHANG Jie RAO Wen-Bo WANG Shao-Chao and LI Xiao-Juan |
| |
| Affiliation: | College of Information Science & Technology, Beijing University of Chemical Technology, Beijing 100029, China,College of Information Science & Technology, Beijing University of Chemical Technology, Beijing 100029, China,College of Information Science & Technology, Beijing University of Chemical Technology, Beijing 100029, China and Capital Normal University, Beijing 100029, China |
| |
| 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. |
| |
| Keywords: | theorem proving formal method high-order logic multiplier HOL4 formal modeling |
|
| 点击此处可从《计算机系统应用》浏览原始摘要信息 |
|
点击此处可从《计算机系统应用》下载全文 |
|
