Abstract
The complexity of railway control system makes some requirement deficiencies hard to find, which results in system failures. It is essential to locate those deficiencies using logs recorded during failure events. In this paper, a model checking based failure analysis approach was proposed and applied to a case of abnormal emergency brake. First, a system model describing the system requirement and an event model depicting the logs were constructed. Next the compositional model was verified through model checking in UPPAAL which then produced a counterexample trace that describes the system behaviour in the failure event. By analysing this trace, an inadequacy was found in the requirement and a modification strategy was brought up which was formally verified to be effective.
This is a preview of subscription content, log in via an institution to check access.
Access this chapter
Tax calculation will be finalised at checkout
Purchases are for personal use only
Similar content being viewed by others
Notes
- 1.
Interlocking (IL) is a widely used signalling system which works together with CTCS-3 to ensure safety, while not included in it.
- 2.
It is only possible when each root event has different intermediate event directly connected to it. We will make it an assumption in this paper.
- 3.
Other solutions are possible, like the one suggested in CTCS-3 technical scheme that track state information is transferred though RBCs.
- 4.
When a train receives a CEM, it will first check if it has already passed the end of this CEM, then initiate an emergency brake if not, or ignore this CEM otherwise.
References
Alur, R., Dill, D.: Automata for modeling real-time systems. In: Paterson, M. (ed.) ICALP 1990. LNCS, vol. 443, pp. 322–335. Springer, Heidelberg (1990)
Bengtsson, J., Larsen, K., Larsson, F., Pettersson, P., Yi, W.: UPPAAL a tool suite for automatic verification of real-time systems. In: Alur, R., Sontag, E.D., Henzinger, T.A. (eds.) HS 1995. LNCS, vol. 1066, pp. 232–243. Springer, Heidelberg (1996)
Bengtsson, J.E., Yi, W.: Timed automata: semantics, algorithms and tools. In: Desel, J., Reisig, W., Rozenberg, G. (eds.) Lectures on Concurrency and Petri Nets. LNCS, vol. 3098, pp. 87–124. Springer, Heidelberg (2004)
Bozzano, M., Villafiorita, A.: The fsap/nusmv-sa safety analysis platform. Int. J. Softw. Tools Technol. Transf. 9(1), 5–24 (2007)
Chuah, E., Kuo, S.h., Hiew, P., Tjhi, W.C., Lee, G., Hammond, J., Michalewicz, M.T., Hung, T., Browne, J.C.: Diagnosing the root-causes of failures from cluster log files. In: 2010 International Conference on High Performance Computing (HiPC), pp. 1–10. IEEE (2010)
Clarke, E.M., Grumberg, O., Peled, D.: Model Checking. MIT Press, Cambridge (1999)
En, N.C.: 50129: Railway application-communications, signaling and processing systems-safety related electronic systems for signaling. British Standards (2003)
Fenelon, P., McDermid, J.A.: New directions in software safety: Causal modelling as an aid to integration. In: Workshop on Safety Case Construction, York, March 1994. Citeseer (1992)
Leveson, N.G., Harvey, P.R.: Software fault tree analysis. J. Syst. Softw. 3(2), 173–181 (1983)
Ming, L.: Fault Location Research Based on Model Checking. Master’s thesis, Central China Normal University (2010)
Platzer, A., Quesel, J.-D.: European train control system: a case study in formal verification. In: Breitman, K., Cavalcanti, A. (eds.) ICFEM 2009. LNCS, vol. 5885, pp. 246–265. Springer, Heidelberg (2009)
Stearley, J.: Towards informatic analysis of syslogs. In: 2004 IEEE International Conference on Cluster Computing, pp. 309–318. IEEE (2004)
Zou, L., Lv, J., Wang, S., Zhan, N., Tang, T., Yuan, L., Liu, Y.: Verifying chinese train control system under a combined scenario by theorem proving. In: Cohen, E., Rybalchenko, A. (eds.) VSTTE 2013. LNCS, vol. 8164, pp. 262–280. Springer, Heidelberg (2014)
Acknowledgement
The work has been supported mainly by the Nation Natural Science Foundation of China (Grant No. 61304185, U1434209), and the National Program on Key Basic Research Project (973 Program) (Grant No. 2014CB340700).
Author information
Authors and Affiliations
Corresponding author
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2016 Springer International Publishing Switzerland
About this paper
Cite this paper
Han, X., Tang, T., Lv, J., Wang, H. (2016). Failure Analysis of Chinese Train Control System Level 3 Based on Model Checking. In: Lecomte, T., Pinger, R., Romanovsky, A. (eds) Reliability, Safety, and Security of Railway Systems. Modelling, Analysis, Verification, and Certification. RSSRail 2016. Lecture Notes in Computer Science(), vol 9707. Springer, Cham. https://doi.org/10.1007/978-3-319-33951-1_7
Download citation
DOI: https://doi.org/10.1007/978-3-319-33951-1_7
Published:
Publisher Name: Springer, Cham
Print ISBN: 978-3-319-33950-4
Online ISBN: 978-3-319-33951-1
eBook Packages: Computer ScienceComputer Science (R0)