Formal Verification for SpaceWire Data Flow Control Using Model Checking

Wei Hua; Xiao Juan Li; Yong Guan; Zhi Ping Shi; Jie Zhang; Ling Ling Dong

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

Paper Titles

Research on Radio Frequency Assignment Mechanism of the RoFSO Network Based on Site-Specific Cognition and Utility Function
p.2439

TDMA-Based Time Slots Assignment Algorithm
p.2445

Hamming Product Code Based Multiple Bit Error Correction Coding Scheme Using Keyboard Scan Based Decoding for on Chip Interconnects Links
p.2457

Design of Open Laboratory Management System Based on RFID
p.2462

Formal Verification for SpaceWire Data Flow Control Using Model Checking
p.2466

A Network Identity Authentication Protocol Based on Fingerprint and Probabilistic Encryption of RSA
p.2471

The Construction and Performance of a Novel Intergroup Complementary Code
p.2475

Binomial Bit-Rate Computation Model Based on Wireless Channel
p.2482

Antenna for Wireless Communications on Unmanned Aerial Vehicles
p.2487

HomeApplied Mechanics and MaterialsApplied Mechanics and Materials Vols. 241-244Formal Verification for SpaceWire Data Flow...

Formal Verification for SpaceWire Data Flow Control Using Model Checking

Abstract:

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.

You might also be interested in these eBooks

Industrial Instrumentation and Control Systems

View Preview

Info:

Periodical:

Applied Mechanics and Materials (Volumes 241-244)

Pages:

2466-2470

DOI:

https://doi.org/10.4028/www.scientific.net/AMM.241-244.2466

Citation:

Cite this paper

Online since:

December 2012

Authors:

Wei Hua, Xiao Juan Li, Yong Guan, Zhi Ping Shi, Jie Zhang, Ling Ling Dong

Keywords:

Error Injection, Formal Verification, FSM, Spacewire Bus Standard, Temporal Logic

Export:

RIS, BibTeX

Price:

Permissions CCC:

Request Permissions

Permissions PLS:

Request Permissions

Сopyright:

Citation:

References

[1] ECSS Standard ECSS-E-ST-50-12C, SpaceWire - Links, Nodes, Routers and Networks [S].

Google Scholar

[2] Liu Tao, HuangWei, Pan Weijun. SpaceWire soft-core design and verification. [J] Journal of Remote Sensing 2011（01）in Chinese.

Google Scholar

[3] Wang Na. Design of SpaceWire Node Interface[D]. Harbin, Heilongjiang: Harbin Institute of Technology , 2007, 7. in Chinese.

Google Scholar

[4] Sanjit A Seshia, Wenchao Li, Subhasish Mitra. Verification-guided soft error resilience[C]. DATE'07 Proceeding of Design, Automation, and Test in Europe, 2007. 4: 1442 – 1447.

DOI: 10.1109/date.2007.364501

Google Scholar

[5] Cadence SMV model checker[S/OL]. http: /www. kenmcmil. com/ smv. html.

Google Scholar

[6] Dai Zhiquan, Formal verification for the system of harsh environment and high-speed bus based on model checking [D]. Beijing: Capital Normal University. 2011. 4. in Chinese.

Google Scholar