Proceedings of 2013 International Conference on Information Science and Computer Applications

Research on Formal Modeling and Verification of on-board ATP System

Authors
Caiyun Chen, Qing Luo, Fang Zhang, Daqing Wang, Xiaoping Xue
Corresponding Author
Caiyun Chen
Available Online October 2013.
DOI
https://doi.org/10.2991/isca-13.2013.5How to use a DOI?
Keywords
Formal verification; SAT problem; Safety property; SCADE
Abstract
Formal software safety verification is an important issue for on-board ATP (Automation Train Protection) system. A SCADE-based model safety formal verification method is designed in this paper. The extracted safety properties of ATP are expressed by formal automaton machine, which is an unambiguous semantics of the formal method ensuring model-based formal verification mechanisms for system safety. Furthermore, the on-board ATP system and the safety properties module are modeled in SCADE suite, and the safety verification by combination of the two models is done in the Design Verifier using SAT-based Bounded model-checking. The advantages of this method are of completeness and can reduce verification costs.
Open Access
This is an open access article distributed under the CC BY-NC license.

Download article (PDF)

Proceedings
2013 International Conference on Information Science and Computer Applications (ISCA 2013)
Part of series
Advances in Intelligent Systems Research
Publication Date
October 2013
ISBN
978-90786-77-85-7
DOI
https://doi.org/10.2991/isca-13.2013.5How to use a DOI?
Open Access
This is an open access article distributed under the CC BY-NC license.

Cite this article

TY  - CONF
AU  - Caiyun Chen
AU  - Qing Luo
AU  - Fang Zhang
AU  - Daqing Wang
AU  - Xiaoping Xue
PY  - 2013/10
DA  - 2013/10
TI  - Research on Formal Modeling and Verification of on-board ATP System
BT  - 2013 International Conference on Information Science and Computer Applications (ISCA 2013)
PB  - Atlantis Press
UR  - https://doi.org/10.2991/isca-13.2013.5
DO  - https://doi.org/10.2991/isca-13.2013.5
ID  - Chen2013/10
ER  -