Modeling of Handover Process in Operation Control System of Maglev Train Using Timed Automata

DOI

10.2991/caai-17.2017.12How to use a DOI?

Keywords

timed auotomata; maglev train; operation control system; handover

Abstract

The OCS (operation control system) is playing a vital role in ensuring the high efficiency and safety of the maglev train. In this paper, we focused on modeling and verification of the handover process of OCS. After we analyzed the function and performance of the system, the process was modeled as a network of timed automata by the verification tool UPPAAL, which was synchronized to describe the communication establishment and massage exchange among subsystems. Then, some key properties that are vital to guarantee the correctness of the handover process were verified with the UPPAAL. Finally, the result shows that the handover process in operation control system of maglev train is provided with safety and restricted activity.

Copyright

© 2017, the Authors. Published by Atlantis Press.

Open Access

This is an open access article distributed under the CC BY-NC license (http://creativecommons.org/licenses/by-nc/4.0/).

Download article (PDF)

TY  - CONF
AU  - Hongze Xu
AU  - Yelei Li
AU  - Liu Jianfeng
PY  - 2017/06
DA  - 2017/06
TI  - Modeling of Handover Process in Operation Control System of Maglev Train Using Timed Automata
BT  - Proceedings of the 2017 2nd International Conference on Control, Automation and Artificial Intelligence (CAAI 2017)
PB  - Atlantis Press
SP  - 60
EP  - 63
SN  - 1951-6851
UR  - https://doi.org/10.2991/caai-17.2017.12
DO  - 10.2991/caai-17.2017.12
ID  - Xu2017/06
ER  -