| SpaceWire译码电路在HOL4中的形式化验证 |
| |
| 引用本文： | 张玉鹏,施智平,关永,李黎明,赵春娜,张杰.SpaceWire译码电路在HOL4中的形式化验证[J].小型微型计算机系统,2013,34(8). |
| |
| 作者姓名： | 张玉鹏 施智平 关永 李黎明 赵春娜 张杰 |
| |
| 作者单位： | 1. 高可靠嵌入式系统技术北京市工程研究中心首都师范大学信息工程学院,北京,100048
2. 北京化工大学信息科学与技术学院,北京,100029 |
| |
| 基金项目： | 国际科技合作计划项目，国家自然科学基金项目，北京市自然科学基金暨北京市教委重点项目，北京市优秀人才培养项目资助 |
| |
| 摘 要： | SpaceWire是在苛刻环境下的高速通信总线协议,译码电路是其接收端的关键电路,对该电路进行形式化验证具有重要的现实意义.形式化验证方法中的定理证明将需要分析的电路进行形式化建模,结合定理证明器,对模型的性质进行严格推理从而完成验证.本文运用定理证明的方法,在高阶逻辑证明工具HOL4中对SpaceWire总线的译码电路进行形式化验证.首先根据SpaceWire标准规范抽取相关性质,用高阶逻辑语言形式化描述；然后分析电路设计中的VHDL代码,依据代码实现的功能用相应的逻辑谓词建模；最后在HOL4中证明了译码电路设计的模型能满足所提取的性质.本文同时给出了形式化建模的方法和验证过程.
|
| 关 键 词： | SpaceWire标准 形式化验证 定理证明 HOL |
Formal Verification of SpaceWire Decoding Circuit in HOL4 |
| |
| ZHANG Yu-peng
,
SHI Zhi-ping
,
GUAN Yong
,
LI Li-ming
,
ZHAO Chun-na
,
ZHANG Jie.Formal Verification of SpaceWire Decoding Circuit in HOL4[J].Mini-micro Systems,2013,34(8). |
| |
| Authors: | ZHANG Yu-peng SHI Zhi-ping GUAN Yong LI Li-ming ZHAO Chun-na ZHANG Jie |
| |
| Abstract: | |
| |
| Keywords: | SpaceWire standard formal verification theorem proving HOL4 |
| 本文献已被 万方数据 等数据库收录！ |
|
