用LTL模型检验的方法验证SpaceWire检错机制

作     者：董玲玲 关永 李晓娟 施智平 张杰 华伟 DONG Lingling;GUAN Yong;LI Xiaojuan;SHI Zhiping;ZHANG Jie;HUA Wei

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

出 版 物：《计算机工程与应用》 (Computer Engineering and Applications)

年 卷 期：2012年第48卷第22期

页      面：88-94页

核心收录：

学科分类：08[工学] 0835[工学-软件工程] 081202[工学-计算机软件与理论] 0812[工学-计算机科学与技术（可授工学、理学学位）] 

基　　金：国际科技合作项目(No.2011DFG13000) 科技部国际科技合作项目(No.2010DFB10930) 北京市教委科技发展项目经费资助(No.KZ201210028036) 北京自然科学基金(No.4122017) 国家自然科学基金(No.61170304) 

主　　题：形式化验证 SpaceWire标准 模型检验 分支时态逻辑(CTL) 线性时态逻辑(LTL) 

摘      要：SpaceWire是应用于航空航天领域的高速通信总线协议,对SpaceWire设计正确性与可靠性要求极高,由于传统的验证方法,存在不完备性等缺陷,对SpaceWire的严格验证一直是备受关注的问题之一。模型检验以其验证的完备性得到设计人员的重视。提出用线性时态逻辑(LTL)模型检验的方法验证SpaceWire系统的检错机制。在检错模块中,该方法与用分支时态逻辑(CTL)验证方法相比,BDD分配数和状态数明显减少,提高了验证效率,还验证了错误优先级;对检错模块处理的五种错误的发生进行验证,验证结果均为正确。该方法实现了对检错机制的完备性验证。