Paper Title:
SpaceWire State Machine Verification Based on Model Checking
  Abstract

SpaceWire is a high-speed data transmission bus standard proposed by ESA for the aerospace applications. Hosted by the National Astronomical Observatories, Chinese Academy of Sciences, the Space Solar Telescope project takes the SpaceWire bus standard as space communication link. The SpaceWire communication circuit implemented by our group is a part of the SST project. In order to improve the fault detection and fault correction capacity and the reliability of the SpaceWire bus, we add a more error analysis and data storage module into the original six state modules of the standard protocol in the exchange layer.We adopt the formal verification method based on the model checking to verify the finite state machine of the SpaceWire control module. The properties expressed by the high-order temporal logic formula are verified automatically to be true by the SMV model verifier of the Cadence Company. Verification results show that our SpaceWire bus implementation and the additional error analysis and data storage module are faithful to the protocol specification. Therefore, we also can integrate SpaceWire bus circuit into the SST project.

  Info
Periodical
Edited by
Qi Luo
Pages
2192-2196
DOI
10.4028/www.scientific.net/AMM.55-57.2192
Citation
Z. Q. Dai, Y. Guan, S. Z. Jin, Z. P. Shi, X. J. Li, J. Zhang, "SpaceWire State Machine Verification Based on Model Checking", Applied Mechanics and Materials, Vols. 55-57, pp. 2192-2196, 2011
Online since
May 2011
Export
Price
$32.00
Share

In order to see related information, you need to Login.

In order to see related information, you need to Login.

Authors: Zhong Liang Pan, Ling Chen
Abstract:The formal verification is able to check whether the implementation of a circuit design is functionally equivalent to an earlier version...
1040
Authors: Yu Ying Yuan, Yong Gang Luo
Chapter 12: Computer-Aided Design, Manufacturing and Engineering
Abstract:Logic design and verification is the frontend of ASIC (Application Specific Integrated Circuit), and is a very important design part during...
4578
Authors: Jie Zhang, Jian Qi, Yong Guan
Chapter 8: Computer-Aided Design and Simulation
Abstract:This paper first summarizes the existing basic theories and methods of hardware design verification. Then it analyzes and compares the...
1208
Authors: Wei Hua, Xiao Juan Li, Yong Guan, Zhi Ping Shi, Jie Zhang, Ling Ling Dong
Chapter 18: Communication Technology and Network Security
Abstract:SpaceWire is a high-speed, full-duplex serial bus standard which is applied in aerospace, so its functions require high accuracy. The...
2466
Authors: Juan Zhang, Guo Qi Li, Xiao Liu
Chapter 3: Information Technologies, WEB and Networks Engineering, Information Security, E-Engineering, Software Application and Development
Abstract:Safety-critical system attracts more attention in recent years. During the development of safety-critical systems, verification plays the...
1227