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

• 作者: 关永 华伟 张杰 施智平 李晓娟 董玲玲
• 来源期刊: 计算机应用与软件
• 学科: 工学
• 关键词: 组合验证 假设保证 模型检验 SpaceWire总线标准 环境状态机
• 年，卷（期）: 2013,（10）
• 所属期刊栏目: 基金项目论文
• 页码范围: 12-15,20
• 页数: 5页
• 分类号: TP302
• 字数: 3638字
• 语种: 中文
• DOI: 10.3969/j.issn.1000-386x.2013.10.004

摘要

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

作者信息

序号	姓名	单位	发文数	被引次数	H指数	G指数
1	张杰	北京化工大学信息科学与技术学院	60	501	11.0	20.0
2	关永	首都师范大学高可靠嵌入式系统技术北京市工程研究中心	95	1336	17.0	33.0
3	李晓娟	首都师范大学高可靠嵌入式系统技术北京市工程研究中心	39	261	9.0	14.0
4	施智平	首都师范大学高可靠嵌入式系统技术北京市工程研究中心	24	145	8.0	11.0
5	董玲玲	首都师范大学高可靠嵌入式系统技术北京市工程研究中心	2	14	2.0	2.0
6	华伟	首都师范大学高可靠嵌入式系统技术北京市工程研究中心	2	14	2.0	2.0