Formal Modeling and Verification of the Functionality of Electronic Urban Railway Control Systems Through a Case Study

Abstract

This paper presents a formal model-based methodology to support railway engineers in the design of safe electronic urban railway control systems. The purpose of our research is to overcome the deficiencies of existing traditional design methodologies, namely the incompleteness and the potential presence of contradictions in the system specification resulting from non-formal development techniques. We illustrate the application of the methodology via a case study of a tram-road level crossing protection system. It was chosen partly because it has a simple architecture and a small number of elements, thus it fits the scope limitations of this article. At the same time, it is suitable for presenting all essential features of our methodology. The proposed solution provides a specification/verification environment that facilitates the construction of correct, complete, consistent, and verifiable functional specifications during the development, while hiding all the formal method-related details from the railway engineers writing the specifications. Using this formal model-based methodology, a high-quality functional specification can be achieved, which is guaranteed to be more exhaustive and will contain fewer errors than traditional development.

Keywords

Requirement specifications / Statechart / Model checking / Safety critical / Urban railway control

References

[1] CENELEC EN 50129:2018 Railway applications – Communication, signaling and processing systems – Safety related electronic systems for signaling (English version).

[2] CENELEC EN 50128:2011 Railway applications – Communication, signaling and processing systems – Software for railway control and protection systems (English version).

[3] Vyatkin V, Hanisch H (2001) Formal modeling and verification in the software engineering framework of IEC 61499: a way to self-verifying systems, In: ETFA 2001. 8th international conference on emerging technologies and factory automation. Proceedings (Cat. No.01TH8597), vol. 2, pp. 113–118. https://doi.org/10.1109/ETFA.2001.997677.

[4] Gnesi S; Margaria T (2013) Some trends in formal methods applications to railway signaling, In: Formal methods for industrial critical systems: a survey of applications, IEEE, pp. 61–84, doi: https://doi.org/10.1002/9781118459898.ch4.

[5] Alanazi MN (2009) Basic rules to build correct UML diagrams, In: 2009 international conference on new trends in information and service science, pp. 72–76. https://doi.org/10.1109/NISS.2009.252

[6] Laibinis L, Troubitsyna E, Leppänen S, Lilius J, Malik Q (2005) Formal model-driven development of communicating systems. In: Lau KK, Banach R (eds) Formal methods and software engineering. ICFEM 2005. Lecture Notes in Computer Science, vol. 3785. Springer, Berlin, Heidelberg. https://doi.org/10.1007/11576280_14.

[7] Clarke EM, Wang Q (2015) 25 years of model checking. In: Voronkov A, Virbitskaite I (eds) Perspectives of system informatics. PSI 2014. Lecture Notes in Computer Science, vol. 8974. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-662-46823-4_2.

[8] IEC 61508-1:2010 Functional safety of electrical/electronic/programmable electronic safety-related systems – Part 1: General requirements (English version).

[9] ISO 26262:2018 Road vehicles – functional safety – from Part 3 to 8 (English version).

[10] DO-178B:2012 Software Considerations in Airborne Systems and Equipment Certification (English version)

[11] CENELEC EN 50126:2017 Railway applications – The Specification and Demonstration of Reliability, Availability, Maintainability and Safety (RAMS) – Part 1: Generic RAMS Process (English version).

[12] A. van Lamsweerde Requirements Engineering: From System Goals to UML Models to Software Specifications, 2009, ISBN: 978-0-470-01270-3.

[13] Colin H (2007) Requirements management, The interface between requirements development and all other systems engineering processes, Springer-Verlag Berlin and Heidelberg GmBH & Co. KG, ISBN: 9783540476894

[14] IBM Rational DOORS (2013) Requirements management framework add-on, user manual, release 6.1. https://www.ibm.com/support/pages/rational-doors-requirements-management-framework-add-61

[15] RequirementOne ReqMan: Getting started guide v1.1., https://www.em.ag/en/reqman/

[16] Siemens Polarion 21 R1 Administrator and User Help, 2021, http://www.teamlive.com.cn/downloads/Polarion_User_and_Administration_Help.pdf

[17] CENELEC EN 50617-2:2015 Railway applications. Technical parameters of train detection systems for the interoperability of the trans-European railway system. Part 2: Axle counters (English version).

[18] Commission Regulation (EU) 2016/919 of 27 May 2016 on the technical specification for interoperability relating to the ‘control command and signaling’ subsystems of the rail system in the European Union

[19] 18/1998. (VII. 3.) KHVM regulation of the National Railway Regulations II volume (Hungary)

[20] Long D, Scott Z (2011) A primer for model-based systems engineering, 2nd edition, ISBN 978-1-105-58810-5

[21] Heinrich H (2011) Model-driven development of advanced user interfaces, ISBN13: 9783642145612. https://doi.org/10.1007/978-3-642-14562-9

[22] Hunt BR, Lipsman RL, Rosenberg Jm, et al (2001) A guide to MATLAB for beginners and experienced users, Cambridge University, ISBN-13: 978-0-511-07792-0

[23] Chaturvedi DK (2010) Modeling and simulation of systems using MATLAB and simulink, ISBN 9781439806722

[24] Papke BL Implementing MBSE – an enterprise approach to an enterprise problem. INCOSE Int Symp, 2020, 30(1): 1550-1567

[25] Selic B (2006) Model-driven development: its essence and opportunities, In: Ninth IEEE international symposium on object and component-oriented real-time distributed computing (ISORC'06), p. 7. https://doi.org/10.1109/ISORC.2006.54.

[26] SEBoK Editorial Board (2022) The guide to the systems engineering body of knowledge (SEBoK), In: Cloutier RJ (Editor in Chief). v. 2.6, The Trustees of the Stevens Institute of Technology, Hoboken. www.sebokwiki.org

[27] Bock C, Cook C (lead), Rivett P, Rutt T, Seidewitz E, Selic B, Tolbert D (2017) OMG Unified Modeling Language (OMG UML) (2017) Version 2.5.1

[28] Holt J, Perry S (2013) SysML for model-based systems engineering, Institution of Engineering and Technology, ISBN: 1849196516. https://doi.org/10.1049/PBPC010E

[29] Wang J, Tepfenhart W (2019) Formal methods in computer science, ISBN 9781498775328

[30] Bartha T, Majzik I (2019) Formal methods for safety planning and proof, ISBN: 978-963-454-2919, doi: https://doi.org/10.1556/9789634542919

[31] Menezes J, Gusmão C, Moura H. Risk factors in software development projects: a systematic literature review. Software Qual J, 2019, 27: 1149-1174

[32] Haxthausen AE (2010) An introduction to formal methods for development of safety-critical applications, DPU Informatics, Technical University of Denmark

[33] Xie Y (2019) Formal modeling and verification of train control systems, Thesis, Centrale Lille

[34] Adacore, QGen User Guide, Release 24.0w (2018) https://docs.adacore.com/live/wave/qgen/pdf/qgen_ug/qgen_ug.pdf

[35] Clarke EM, Henzinger TA, Veith H (2018) Introduction to model checking. In: Clarke E, Henzinger T, Veith H, Bloem R (eds) Handbook of Model Checking. Springer, Cham. https://doi.org/10.1007/978-3-319-10575-8_1

[36] Newborn M, Automated theorem proving, theory and practice, Springer New York, NY, ISBN-10: 0387950753. https://doi.org/10.1007/978-1-4613-0089-2

[37] Terada N, Toyama T (2013) Application of verification methods to specifications of signalling equipment, quarterly report of RTRI, 2013, Volume 54, Issue 4, Pages 202-207, Released December 05, 2013, Online ISSN 1880-1765, Print ISSN 0033-9008. https://doi.org/10.2219/rtriqr.54.202

[38] Zou L et al (2014) Verifying Chinese train control system under a combined scenario by theorem proving. In: Cohen E, Rybalchenko A (eds.) Verified software: theories, tools, experiments. VSTTE 2013. Lecture Notes in Computer Science, vol. 8164. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-642-54108-7_14.

[39] Stankaitis P, Dupont G, Singh NK, Ait-Ameur Y, Iliasov A, Romanovsky A (2019) Modelling hybrid train speed controller using proof and refinement, In: 2019 24th international conference on engineering of complex computer systems (ICECCS), pp. 107–113. https://doi.org/10.1109/ICECCS.2019.00019.

[40] Eisner C. Using symbolic CTL model checking to verify the railway stations of Hoorn-Kersenboogerd and Heerhugowaard. STTT, 2002, 4: 107-124

[41] Eisner C (1999) Using symbolic model checking to verify the railway stations of Hoorn-Kersenboogerd and Heerhugowaard. In: Pierre L, Kropf T (eds.) Correct hardware design and verification methods. CHARME 1999. Lecture Notes in Computer Science, vol 1703. Springer, Berlin, Heidelberg. https://doi.org/10.1007/3-540-48153-2_9

[42] Haxthausen A, Peleska J (2015) Model checking and model-based testing in the railway domain. In: Drechsler R, Kühne U (eds.) Formal modeling and verification of cyber-physical systems. Springer Vieweg, Wiesbaden. https://doi.org/10.1007/978-3-658-09994-7_4

[43] Halpern JY, Vardi MY (1991) Model checking vs. theorem proving: a manifesto, KR. https://doi.org/10.1016/B978-0-12-450010-5.50015-3

[44] Kunnappilly A, Backeman P, Seceleanu C (2021) From UML modeling to UPPAAL model checking of 5G dynamic service orchestration, In: ECBS 2021, Conference on the engineering of computer based systems. https://doi.org/10.1145/3459960.3459965.

[45] Guo C, Fu Z, Zhang Z, Ren S, Sha L (2020) A framework for supporting the development of verifiably safe medical best practice guideline systems, J Syst Archit, 104: 101693, ISSN 1383-7621.https://doi.org/10.1016/j.sysarc.2019.101693

[46] David A., Möller MO, Yi W (2002) Formal verification of UML statecharts with real-time extensions. In: Kutsche RD, Weber H (eds.) Fundamental approaches to software engineering. FASE 2002. Lecture Notes in Computer Science, vol 2306. Springer, Berlin, Heidelberg. https://doi.org/10.1007/3-540-45923-5_15

[47] Darvas D (2016) Practice-oriented formal methods to support the software development of industrial control systems. https://doi.org/10.5281/zenodo.162950

[48] Vince M, Bence G, András V, István M, Dániel V (2018) The gamma statechart composition framework: design, verification and code generation for component-based reactive systems. In: Proceedings of the 40th international conference on software engineering companion. ACM Press, New York, pp. 1–4. ISBN 978-1-4503-5663-3 (In Press). https://doi.org/10.1145/3183440.3183489.

[49] Graics B, Molnár V, Vörös A Mixed-semantics composition of statecharts for the component-based design of reactive systems. Softw Syst Model, 2020, 19: 1483-1517

[50] Jiang Y et al (2016) From stateflow simulation to verified implementation: a verification approach and a real-time train controller design, In: 2016 IEEE real-time and embedded technology and applications symposium (RTAS), pp. 1–11.https://doi.org/10.1109/RTAS.2016.7461337

[51] Nazaruddin YY, Tamba TA, Pradityo K, Aristyo B, Widyotriatmo A (2019) Safety verification of a train interlocking timed automaton model, IFAC-PapersOnLine, 52(15): 331-335, ISSN 2405-8963, https://doi.org/10.1016/j.ifacol.2019.11.696

[52] Keming W, Zheng W, Chuandong Z (2018) Formal modeling and data validation of general railway interlocking system, In: 16th internal conference on railway engineering design & operation, lisbon, Portugal, 181: 527–538, ISSN 1743-3509. https://doi.org/10.2495/CR180471.

[53] Cooper K, Ito MR (2002) Formalizing a structured natural language requirements specification notation, INCOSE International Symposium 12. https://doi.org/10.1002/j.2334-5837.2002.tb02569.x

[54] Lukács G, Bartha T (2022) Practical UML subset for railway engineers to support formal modeling. Trans Motauto World 7(2):56–59

[55] Baier C, Katoen J-P (2008) Principles of model checking. The MIT Press

[56] Chatterjee K, Doyen L (2016) Computation tree logic for synchronization properties, In: 43rd International colloquium on automata, languages, and programing (ICALP 2016). https://doi.org/10.48550/arXiv.1604.06384

[57] Behrmann G, David A, Larsen KG (2004) A tutorial on UPPAAL. In: Bernardo M, Corradini F (eds) Formal methods for the design of real-time systems. SFM-RT 2004. Lecture notes in computer science, vol 3185. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-540-30080-9_7

[58] Lukács G, Bartha T (2021) Formal modelling of level crossing system for tramsusing UPPAAL framework, Technical Review (EMT) 77: 18–37, 20 p

[59] Bensalem S, Bozga M, Sifakis J, Nguyen TH (2008) Compositional verification for component-based systems and application. In: Cha S, Choi JY, Kim M, Lee I, Viswanathan M (eds) Automated technology for verification and analysis. ATVA 2008. Lecture Notes in Computer Science, vol 5311. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-540-88387-6_7

[60] Boehm B, Port D, Winsor Brown A. Balancing plan-driven and agile methods in software engineering project courses. Comput Sci Educ, 2002, 12(3): 187-195

[61] Asagba PO, Ogheneovo EE (2007) A comparative analysis of structured and obejct-oriented programming methods, African J (AJOL), 11(4). https://doi.org/10.4314/jasem.v11i4.55190

[62] Campean F, Henshall E, Yildirim U, Uddin A, Williams H (2013) A structured approach for function based decomposition of complex multi-disciplinary systems. In: Abramovici M, Stark R (eds.) Smart product engineering. Lecture Notes in Production Engineering. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-642-30817-8_12

[63] Herrigel S, Laumanns M, Nash A, Weidmann U. Hierarchical decomposition methods for periodic railway timetabling problems. Transp Res Rec, 2013, 2374(1): 73-82

[64] Budapest Transport Privately Held Corporation (BKV) (2011) Requirements booklet for safety elements and equipment for traffic control of trams (BKV-VILL-1.04)

[65] itemis, Yakindu statechart tools, User Guide, https://www.itemis.com/en/yakindu/state-machine/documentation/user-guide/overview_what_are_state_machines?hsLang=de