欢迎您！东篱公司
退出
-
申报数据库
-
立项数据库
-
成果数据库
-
项目获奖数据库
中文摘要：
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 SpaeeWire 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.
同期刊论文项目
同项目期刊论文
Analysis of the Degradation of MOSFETs in Switching Mode Power Supply by Characterizing Source Oscil
Power supply prognostics and health management of high reliability electronic systems in rugged envi
期刊信息
位置：