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

计算机工程与应用 ›› 2012, Vol. 48 ›› Issue (22): 88-94.

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

董玲玲1，关永1，李晓娟1，施智平1，张杰2，华伟1

1.首都师范大学高可靠嵌入式系统技术北京市工程研究中心，北京 100048
2.北京化工大学信息科学与技术学院，北京 100029

出版日期:2012-08-01 发布日期:2012-08-06

Verification for SpaceWire error detection mechanism by LTL model checking

DONG Lingling1, GUAN Yong1, LI Xiaojuan1, SHI Zhiping1, ZHANG Jie2, HUA Wei1

1.Beijing Engineering Research Center of High Reliable Embedded System, Capital Normal University, Beijing 100048, China
2.College of Information Science & Technology, Beijing University of Chemical Technology, Beijing 100029, China

Online:2012-08-01 Published:2012-08-06

摘要/Abstract

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

关键词: 形式化验证, SpaceWire标准, 模型检验, 分支时态逻辑（CTL）, 线性时态逻辑（LTL）

Abstract: SpaceWire is the spacecraft high-speed bus protocol, and widely used in aerospace field, then the correctness and reliability of SpaceWire design are highly demanded. Because the traditional verification methods existence incomplete defects, SpaceWire system verification has become a research focus in the fields. However, model checking is more and more popular among designers because of its complete merits. It proposes the LTL model checking to verify the SpaceWire error detection mechanism. In error detection module, by compared the verification of LTL with CTL, it finds that LTL properties can improve the verification efficiency because of its less number of BDD allocation and state, and also verifies error priority. In addition, it verifies appearance of five errors, and the results are true. So this method realizes complete validation of the error detection mechanism.

Key words: formal verification, SpaceWire standard, model checking, Computional Tree Logic（CTL）, Linear Temporal Logic（LTL）

董玲玲1，关永1，李晓娟1，施智平1，张杰2，华伟1. 用LTL模型检验的方法验证SpaceWire检错机制[J]. 计算机工程与应用, 2012, 48(22): 88-94.

DONG Lingling1, GUAN Yong1, LI Xiaojuan1, SHI Zhiping1, ZHANG Jie2, HUA Wei1. Verification for SpaceWire error detection mechanism by LTL model checking[J]. Computer Engineering and Applications, 2012, 48(22): 88-94.

[1]	孙浩然1，2，施智平1，2，3，关永1，3，王瑞2，3. 穿刺机器人运动安全性的形式化分析与建模[J]. 计算机工程与应用, 2018, 54(18): 263-270.
[2]	李群，陈清亮. 基于ATL的公平交换协议的形式化验证[J]. 计算机工程与应用, 2015, 51(19): 32-36.
[3]	田野，曾红卫. 用模型检验产生约简测试集[J]. 计算机工程与应用, 2012, 48(17): 93-98.
[4]	李仁见，王昭飞. 命令式程序终止性验证方法综述[J]. 计算机工程与应用, 2011, 47(28): 1-6.
[5]	林基艳，吴振强. 并行分类信任链传递模型[J]. 计算机工程与应用, 2009, 45(31): 98-101.
[6]	谭亮,曾红卫. 基于接口自动机的Web应用验证[J]. 计算机工程与应用, 2009, 45(3): 70-73.
[7]	刘恩军. 基于线性带权值的广义表的模型检验方法[J]. 计算机工程与应用, 2008, 44(29): 88-91.
[8]	曾琼¹,黄健^2,3,魏乐^2,3. 基于吴方法的符号模型检验[J]. 计算机工程与应用, 2008, 44(27): 46-48.
[9]	王金双,杨华兵,张兴元,王元元,张毓森. 电梯控制系统在Isabelle/HOL中的活动性证明[J]. 计算机工程与应用, 2008, 44(27): 216-218.
[10]	高新岩¹,吴尽昭¹,闫炜¹,周宁². 非经典切片技术及其在形式验证中的应用综述[J]. 计算机工程与应用, 2007, 43(36): 43-47.
[11]	屈婉霞,李暾,郭阳,杨晓东. 模型检验中抽象技术研究综述[J]. 计算机工程与应用, 2006, 42(33期): 15-19.