基于假设保证的SpaceWire总线链路接口的组合验证

作     者：华伟 李晓娟 关永 施智平 张杰 董玲玲 Hua Wei;Li Xiaojuan;Guan Yong;Shi Zhiping;Zhang Jie;Dong Lingling

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

基　　金：国家自然科学基金项目(60873006 61070049 61170304 61104035) 北京市自然科学基金暨北京教委重点项目(4122017 KZ201210028036) 国际科技合作计划项目(2010DFB10930 2011DFG13000) 

出 版 物：《计算机应用与软件》 (Computer Applications and Software)

年 卷 期：2013年第30卷第10期

页      码：12-15,20页

摘      要：SpaceWire是一种面向航天应用的高速、全双工的串行总线标准,对其功能正确性的实现具有极高需求。运用模型检验的方法对SST项目中SpaceWire总线链路接口的设计实现与标准规范的一致性进行形式化的验证。在对SpaceWire总线链路接口进行形式建模时,运用假设保证推理,通过抽象环境状态机,建立层次化的组合验证模型,实现了关键功能属性的验证,并有效地解决了状态爆炸问题,缩短验证时间。该方法克服了模拟和测试等传统验证方法的不完备性,为验证SpaceWire总线链路接口设计与实现的功能正确性提供了有效的验证手段。

主 题 词：组合验证 假设保证 模型检验 SpaceWire总线标准 环境状态机 

学科分类：08[工学] 081201[081201] 0812[工学-测绘类] 

核心收录：

D　O　I：10.3969/j.issn.1000-386x.2013.10.004

馆 藏 号：203889031...