Formal Verification for SpaceWire Data Flow Control Using Model Checking

被引：0

作者：

Hua, Wei ^{[1
]}

Li, Xiaojuan ^{[1
]}

Guan, Yong ^{[1
]}

Shi, Zhiping ^{[1
]}

Zhang, Jie ^{[2
]}

Dong, Lingling ^{[1
]}

机构：

[1] Capital Normal Univ, Coll Informat Engn, Beijing 100048, Peoples R China

[2] Beijing Univ Chem Technol, Coll Informat Sci & Technol, Beijing 100029, Peoples R China

来源：

INDUSTRIAL INSTRUMENTATION AND CONTROL SYSTEMS, PTS 1-4 | 2013年 / 241-244卷

基金：

中国国家自然科学基金; 北京市自然科学基金;

关键词：

Formal verification; SpaceWire bus standard; Temporal logic; FSM; Error injection;

D O I：

10.4028/www.scientific.net/AMM.241-244.2466

中图分类号：

TP [自动化技术、计算机技术];

学科分类号：

0812 ;

摘要：

SpaceWire is a high-speed, full-duplex serial bus standard which is applied in aerospace, so its functions require high accuracy. The traditional methods of verification, such as simulation and test, are not complete. In order to prove the design of the SpaceWire faithfully implemented the SpaceWire protocol's specification, we presented our experience on the model checking of SpaceWire data flow control using the Cadence SMV tool. It overcomes the incompleteness of traditional verification. And by injecting the errors to ensure the accuracy of the artificial extraction properties and completeness, comparison tests show that the method can effectively ensure the functional coverage, improve reliability of the verification.

引用

页码：2466 / +

页数：2