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）

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

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