中文摘要：

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

英文摘要：

SpaceWire is the spacecraft high-speed bus protocol, and widely used in aerospace field, then the correct- ness and reliability of SpaceWire design are highly demanded. Because the traditional verification methods exis- tence 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 verifica- tion 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.