论文研究多路径覆盖测试数据生成适应度函数设计方法.pdf

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