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

摘要：

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

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

所属期刊栏目：48

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

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

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

页数：共7页

页码：88-94