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

摘要：

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

关键词：SpaceWire标准、形式化验证、定理证明、HOL

所属期刊栏目：34

分类号：TP309(计算技术、计算机技术)

资助基金：国际科技合作计划项目2010DFB10930,2011DFG13000;国家自然科学基金项目60873006,61070049,61170304,61104035;北京市自然科学基金暨北京市教委重点项目4122017,KZ201210028036;北京市优秀人才培养项目资助

在线出版日期：2013-11-05（万方平台首次上网日期，不代表论文的发表时间）

页数：共5页

页码：1959-1963