SpaceWire译码电路在HOL4中的形式化验证

• 作者: 关永 张杰 张玉鹏 施智平 李黎明 赵春娜
• 来源期刊: 小型微型计算机系统
• 学科: 工学
• 关键词: SpaceWire标准 形式化验证 定理证明 HOL
• 年，卷（期）: 2013,（8）
• 所属期刊栏目: 计算机体系结构及其他
• 页码范围: 1959-1963
• 页数: 5页
• 分类号: TP309
• 字数: 4151字
• 语种: 中文

摘要

SpaceWire是在苛刻环境下的高速通信总线协议,译码电路是其接收端的关键电路,对该电路进行形式化验证具有重要的现实意义.形式化验证方法中的定理证明将需要分析的电路进行形式化建模,结合定理证明器,对模型的性质进行严格推理从而完成验证.本文运用定理证明的方法,在高阶逻辑证明工具HOL4中对SpaceWire总线的译码电路进行形式化验证.首先根据SpaceWire标准规范抽取相关性质,用高阶逻辑语言形式化描述；然后分析电路设计中的VHDL代码,依据代码实现的功能用相应的逻辑谓词建模；最后在HOL4中证明了译码电路设计的模型能满足所提取的性质.本文同时给出了形式化建模的方法和验证过程.

作者信息

序号	姓名	单位	发文数	被引次数	H指数	G指数
1	张杰		60	501	11.0	20.0
2	施智平	高可靠嵌入式系统技术北京市工程研究中心首都师范大学信息工程学院	4	16	2.0	4.0
3	关永	高可靠嵌入式系统技术北京市工程研究中心首都师范大学信息工程学院	3	16	2.0	3.0
4	李黎明	高可靠嵌入式系统技术北京市工程研究中心首都师范大学信息工程学院	2	10	2.0	2.0
5	张玉鹏	高可靠嵌入式系统技术北京市工程研究中心首都师范大学信息工程学院	1	8	1.0	1.0
6	赵春娜	高可靠嵌入式系统技术北京市工程研究中心首都师范大学信息工程学院	1	8	1.0	1.0