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

• 作者: 关永 华伟 张杰 施智平 李晓娟 董玲玲
• 来源期刊: 计算机工程与应用
• 学科: 工学
• 关键词: 形式化验证 SpaceWire标准 模型检验 分支时态逻辑(CTL) 线性时态逻辑(LTL)
• 年，卷（期）: 2012,（22）
• 所属期刊栏目: 研发、设计、测试
• 页码范围: 88-94
• 分类号: TP311
• 字数: 5071字
• 语种: 中文
• DOI: 10.3778/j.issn.1002-8331.2012.22.019

摘要

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

作者信息

序号	姓名	单位	发文数	被引次数	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