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

摘要

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.