运用定理证明的形式化方法验证SpaceWire编码电路  

Formal Method for Verifying SpaceWire Encoding Circuit by Applying Theorem Proving

作　　者：李黎明[1] 关永[1] 吴敏华[1] 张杰[2] 施智平[1] 

机构地区：[1]首都师范大学高可靠嵌入式系统技术北京市工程研究中心,北京100048 [2]北京化工大学信息科学与技术学院,北京100029

出　　处：《小型微型计算机系统》2012年第6期1372-1376,共5页Journal of Chinese Computer Systems

基　　金：国家自然科学基金项目(60873006;61070049;61170304)资助;国际科技合作项目(2010DFB10930)资助;北京市自然科学基金重点项目B类北京市教委科技发展重点项目资助

摘　　要：我国空间太阳望远镜(SST)项目采用了SpaceWire作为传输总线,目前针对SpaceWire总线的验证主要采用测试和模拟等传统的方法,这类验证方法是不完备的.本文旨在对SST项目中SpaceWire总线的DS编码电路是否如实地实现标准中的规范要求进行验证,运用定理证明的形式化方法,在HOL4工具上对该电路的设计实现与规范要求的一致性进行验证,克服了传统验证方法的局限性.SpaceWire bus is applied in Space Solar Telescope （SST） project. Testing and simulation are the main methods for verifi- cation of SpaceWire bus, but these verifications are incomplete. This study focused on verifying whether the DS encoder circuit devel- oped for SST had faithfully implemented the specification in SpaceWire standard. With the aid of HOL4 tool, this equivalence chec- king was carried out in a formal verification method, theorem proving. It overcame the limitation of testing and simulation.

关 键 词：形式化验证 SpaceWire标准 DS编码 定理证明 高阶逻辑 

分 类 号：TP309[自动化与计算机技术—计算机系统结构]