CAJ | 학술논문

SpaceWire是一种面向航天应用的高速、全双工的串行总线标准，对其功能正确性的实现具有极高需求。运用模型检验的方法对 SST项目中SpaceWire 总线链路接口的设计实现与标准规范的一致性进行形式化的验证。在对SpaceWire总线链路接口进行形式建模时，运用假设保证推理，通过抽象环境状态机，建立层次化的组合验证模型，实现了关键功能属性的验证，并有效地解决了状态爆炸问题，缩短验证时间。该方法克服了模拟和测试等传统验证方法的不完备性，为验证SpaceWire总线链路接口设计与实现的功能正确性提供了有效的验证手段。
SpaceWire시일충면향항천응용적고속、전쌍공적천행총선표준，대기공능정학성적실현구유겁고수구。운용모형검험적방법대 SST항목중SpaceWire 총선련로접구적설계실현여표준규범적일치성진행형식화적험증。재대SpaceWire총선련로접구진행형식건모시，운용가설보증추리，통과추상배경상태궤，건립층차화적조합험증모형，실현료관건공능속성적험증，병유효지해결료상태폭작문제，축단험증시간。해방법극복료모의화측시등전통험증방법적불완비성，위험증SpaceWire총선련로접구설계여실현적공능정학성제공료유효적험증수단。
SpaceWire is a high-speed,full-duplex serial bus standard for aerospace applications,so the implementation of its functional correctness has very high demand.We use model checking approach to make the formal verification on the consistency between the design and implementation of SpaceWire bus link interface and the standard specification of SpaceWire in SST project.In formal modelling for the SpaceWire bus link interface,we use assume-guarantee reasoning to build hierarchical combination verification model through abstracted environmental state machine,realise the verification on crucial functional property,and effectively solve the problem of state explosion, shorten the verification time.The approach overcomes the incompleteness of the traditional verification methods such as simulation and test, etc.,provides a valid means for verifying the functional correctness of the design and implementation of the SpaceWire bus link interface.