Author(s)

L. Yuan, T. Tang, K. Li & Y. Liu

Abstract

The interoperability of train control systems is an essential feature for high-speed railways. It must be proven that the on-board system of the train control system has the ability to allow the safe and uninterrupted movement of each line, which accomplishes the specified performance. A third-party interoperability test bench should be built for the customer to test the interoperability of the on-board systems, which are manufactured by different appliers. In this paper, a formal model was applied on the design and the verification of the test bench. The design errors can be detected using this formal model, thus the correctness of the test bench functionality was ensured. A structured Colored Petri Nets model was proposed to describe the test bench in the aspects of system, modules and processes. The model includes three sub-models: test bench, interface and onboard system. Colored Petri Nets was used for system modeling and CPN-TOOLS was used to support the simulation and the formal analysis. The hierarchical modeling method not only reduces the complexity, but also enhances the reliability and reusability. On the basis of these models, the architecture, the information flow and the algorithms of the test bench can be verified during the system design and development. The simulation results showed that the design errors can be found and some algorithms can be verified and corrected in the modeling and simulation process. Keywords: test bench, CPN, formal method, train control system.

Keywords

test bench, CPN, formal method, train control system