基于HOL4的形式化方法

• 作者: 张杰 李晓娟 王少超 饶文博
• 来源期刊: 计算机系统应用
• 关键词: 定理证明 形式化方法 高阶逻辑 乘法器 HOL4 形式化建模
• 年，卷（期）: 2016,（2）
• 所属期刊栏目: 软件技术·算法
• 页码范围: 202-207
• 页数: 6页
• 字数: 3807字
• 语种: 中文

摘要

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

作者信息

序号	姓名	单位	发文数	被引次数	H指数	G指数
1	张杰	北京化工大学信息科学与技术学院	60	501	11.0	20.0
2	李晓娟		39	261	9.0	14.0
3	饶文博	北京化工大学信息科学与技术学院	1	2	1.0	1.0
4	王少超	北京化工大学信息科学与技术学院	2	4	2.0	2.0