Model Checking for SpaceWire Error Detection Module

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

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

Paper Titles

The Application of Data Mining in the Civil Aviation Accident Analysis
p.3000

Prediction for Network Traffic Based on Modified Elman Neural Network
p.3005

3D Medical Images Registration Based on GPU Parallel Computing
p.3010

A Control Algorithm of LCD Dynamic Backlight Based on PSNR
p.3014

Model Checking for SpaceWire Error Detection Module
p.3020

Digital Image Watermarking Based on Second Generation Wavelet Transform
p.3026

Recognition of Surface Roughness Based on Fractal Theory and the Microscopic Images
p.3030

Fast Fractal Image Coding Method Based on RMSE and DCT Classification
p.3034

CIM/XML Format-Based SCADA Data Analysis and Application
p.3040

HomeApplied Mechanics and MaterialsApplied Mechanics and Materials Vols. 241-244Model Checking for SpaceWire Error Detection...

Model Checking for SpaceWire Error Detection Module

Abstract:

Considerable attention has been devoted to prove the correctness of programs. Formal verification overcomes the incompleteness by applying mathematical methods to verify a design. SpaceWire is a well known communication standard. For safety-critical applications an approach is needed to validate the completeness of SpareWire design. This paper addresses formal verification of SpareWire error detection module. The system model was constructed by Kripke structure, and the properties were presented by linear temporal logic (LTL). Compared the verification of LTL with CTL (branch temporal logic), LTL properties could improve the verification efficiency due to its linear search. The error priority was checked using simulation guided by model checking. After some properties were modified, all possible behaviors of the module satisfied the specification. This method realizes complete validation of the error detection module.

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:

3020-3025

DOI:

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

Citation:

Cite this paper

Online since:

December 2012

Authors:

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

Keywords:

CTL, LTL, Model Checking, SMV, SpaceWire

Export:

RIS, BibTeX

Price:

Permissions CCC:

Request Permissions

Permissions PLS:

Request Permissions

Сopyright:

Citation:

References

[1] Saponara, S., Petri, E., Tonarelli, M., Corona, I. D., Fanucci, L., EDA Consortium 2007, pp.480-485.

Google Scholar

[2] Beer, I., Ben-David, S., Eisner, C., Rodeh, Y., Form Method Syst Des 2001, 18, 141-163.

Google Scholar

[3] Peng, H., Tahar, S., Khendek, F., International Journal on Software Tools for Technology Transfer (STTT) 2003, 4, 234-245.

DOI: 10.1007/s100090200073

Google Scholar

[4] Tarrillo, J., Chipana, R., Chielle, E., Kastensmidt, F. L., in: 12th Latin American Test Workshop 2011.

DOI: 10.1109/latw.2011.5985929

Google Scholar

[5] Seshia, S. A., Li, W., Mitra, S., EDA Consortium 2007, pp.1442-1447.

Google Scholar

[6] Dai, Z. Q., Guan, Y., Jin, S. Z., Shi, Z. P., et al., Applied Mechanics and Materials 2011, 55, 2192-2196.

Google Scholar

[7] Emerson, E. A., Halpern, J. Y., Journal of the ACM (JACM) 1986, 33, 151-178.

Google Scholar

[8] Standardization, E. C. F. S., 2003. Information on http://www.spacewire.esa.int/tech/spacewire/standards/.

Google Scholar

[9] Clarke, E., Grumberg, O., Jha, S., Lu, Y., Veith, H., Springer 2001, pp.176-194.

Google Scholar