Functional safety verification of train control procedure in train-centric CBTC by colored petri net
DOI:
https://doi.org/10.5604/01.3001.0014.2730Keywords:
train control procedure, Train-centric CBTC, functional safety, formal methods, colored Petri netAbstract
Communication-based Train Control (CBTC) system is a widely-used signaling system. There is an increasing demand for innovating the traditional ground-centric architecture. With the application of train-train communication, object control and other advanced techniques, Train-centric CBTC (TcCBTC) system is expected to be the most promising tendency of train control system. The safe tracking interval would be reduced as well as the life-cycle costs. Formal methods play an essential role in the development of safety-critical systems, which provides an early integration of the verifiable design process. In the paper, the architecture design of TcCBTC is first analyzed. The official system specification of TcCBTC has not issued, so it takes efforts to perform the systematic summarization of the functional requirements. Secondly, we propose an integrated framework that combines the Colored Petri Net (CPN) models with the functional safety verification of the underlying systems. Functional safety depends on the logic accuracy and is a part of overall safety. The framework also specifies what kinds of functions, behaviors or properties need to be verified. The train control procedure of TcCBTC is regarded as the link among new functional modules, thus it is chosen as the modelling content. Thirdly, the scenarios and the color sets are prepared. Models are established with the novel design thought from top to bottom. Simulation and testing are implemented during the model establishment to discover the apparent errors. Lastly, the model checking by state space is performed. All possible states are checked in detail. Standard behavioral properties and other user-defined properties are verified by state space report and ASK-CTL (Computation Tree Logic) queries, respectively. Verification results reveal that the models are reasonable to depict the dynamic behaviors of train control procedure. The functional safety properties are satisfied and prepared for further drafting the system functional specification.
References
CENELEC. EN 50126-1:2017, Railway applications -Th e specification and demonstration of reliability, availability, maintainability and safety (RAMS) Part 1: Basic requirements and generic process.
CHEN, L.J., TANG, T., et al. 2012.Verification of the safety communication protocol in train control system using colored Petri net. Reliability Engineering and System Safety,100:8-18.
CHEN, M.S., BAO, Y.X., &SUN, H.Y., et al., 2017. Survey on formal method of trustworthy construction for communication-based train control systems. Journal of Software, 28(5):1183-1203.
CHENG, R., ZHOU, J., &CHEN, D., 2016. Model-based verification method for solving the parameter uncertainty in the train control system. Reliability Engineering and System Safety,145:169-182.
DU, H., SUN, G.J., &CHEN, Q., 2017. A new generation CBTC system without CI and ZC. Urban Rapid Rail Transit. 30(04):91-95.
GAO, C.H, 2018.Communication-based Train Control System. China Railway Publishing House. Beijing, (Chapter 10).
HORSTE, M. Z., HUNGAR, H.,& SCHNIEDER E., 2013, Modelling functionality of train control systems using Petri nets, Towards a Formal Methods Body of Knowledge for Railway Control and Safety Systems. Lyngby, Denmark, 46-50.
HOU, T., GUO, Y.Y.,NIU, H.X., 2019, Research on speed control of high-speed train based on multipoint model. Archives of Transport. 50(2), 35-46.
INTERNATIONAL UNION OF RAILWAYS. UIC Homepage: OpenETCS, 2013. [checked on 2020-3-10] URL http://www.uic.org/spip.php?article2998.
JANSEN, K., KRISTENSEN L. M. 2009. Colored Petri Nets: Modelling and Validation of Concurrent Systems. Springer.
JANSEN, L., MEYER M., & SCHNIEDER E.,1998 Technical issues in modelling the ETCS using colored Petri nets and the Design/CPN tools. Proceedings of the workshop on practical use of colored Petri Nets and Design /CPN, 103–115. Aarhus and Denmark.
LI K.,ZHANG X. S, Design and formal verification of safety communication protocol in STP. Computer Engineering,2018,44(12): 120-128．
MEYER, M., PTOK, B., et.al. 2000, A case study for the automated system development: the satellite-based train control system. Proceedings of IFAC Conference on Control Systems Design, 329–334. Bratislava and Slovak Republic.
MORENO, J., RIERA, J. M., & DE HARO, L., et al, 2015. A survey on future railway radio communications services: Challenges and opportunities. IEEE Communication Magazine, 53(10), 62-68.
SONG, H.F., SCHNIEDE, E., 2019.Development and Evaluation Procedure of the Train-Centric Communication-Based System. IEEE Transaction on Vehicular Technology,68(3).
Urbalis Fluence. 2018. [checked on 2020-3-10].URL https://www.alstom.com/urbalis-cbtc-range-future-signalling-systems.
WANG, X.X., LIU, L.J., et al, 2019. Enhancing Communication-Based Train Control Systems Through Train-to-Train Communications. IEEE Transactions on Intelligent Transportation System, 20(4),1544-1561.
WU, D.H., 2014.Verifiable design of a satellite-based train control system with Petri nets (Ph.D. thesis). Germany: Technische Universität Braunschweig.
WU, D.H., SCHNIEDER, E., 2016, Scenario-based modeling of the on-board of a satellite-based train control system with colored Petri net. IEEE Transaction on Intelligent Transportation System,17(11), 3045-3061.
ZHENG, W., 2019. Research on Modelling and Verification of Traincentric Interlocking Control (Master thesis). China: Beijing Jiaotong University.
ZHU, L., YAO, D.Y., &ZHAO, H.L., Reliability analysis of next-generation CBTC data communication systems. IEEE Transactions on Vehicular Technology, 2019, 68(3), pp. 2024-2034.
Downloads
Published
Issue
Section
License
Copyright (c) 2024 Archives of Transport journal allows the author(s) to hold the copyright without restrictions.
This work is licensed under a Creative Commons Attribution 4.0 International License.
How to Cite
