论文部分内容阅读
SpaceWire是一种面向航天应用的高速、全双工的串行总线标准，对其功能正确性的实现具有极高需求。运用模型检验的方法对SST项目中SpaceWire总线链路接口的设计实现与标准规范的一致性进行形式化的验证。在对SpaceWire总线链路接口进行形式建模时，运用假设保证推理，通过抽象环境状态机，建立层次化的组合验证模型，实现了关键功能属性的验证，并有效地解决了状态爆炸问题，缩短验证时间。该方法克服了模拟和测试等传统验证方法的不完备性，为验证SpaceWire总线链路接口设计与实现的功能正确性提供了有效的验