LightF3: A Lightweight Fully-Process Formal Framework for Automated Verifying Railway Interlocking Systems
Authors: 
Yibo Dong, Xiaoyu Zhang, Yicong Xu, Chang Cai, Yu Chen, Weikai Miao, Jianwen Li, Geguang PuAuthors Info & Claims
Pages 1914 - 1925
Abstract
Interlocking has long played a crucial role in railway systems. Its functional correctness, particularly concerning safety, forms the foundation of the entire signaling system. To date, numerous efforts have been made to formally model and verify interlocking systems. However, two main problems persist in most prior work: (1) The formal description of the interlocking system heavily depends on reusing existing models, which often results in overgeneralization and failing to fully utilize the intrinsic characteristics of interlocking systems. (2) The verification techniques of current approaches may quickly become outdated, and there is no adaptable method to integrate state-of-the-art verification algorithms or tools.
To address the above issues, we present LightF3, a lightweight and fully-process formal framework for modeling and verifying railway interlocking systems. LightF3 provides RIS-FL, a formal language based on FQLTL (a variant of LTL) to model the system and its specifications. LightF3 transforms the RIS-FL model automatically to the aiger model, which is the mainstream input of state-of-the-art model checkers, and then invokes the most advanced checkers to complete the verification task. We evaluated LightF3 by testing five real station instances from our industrial partner, demonstrating its effectiveness as a new framework. Additionally, we analyzed the statistics of the verification results from different model-checking techniques, providing useful conclusions for both the railway interlocking and formal methods communities.
References
[1]
[n. d.]. IC3Ref. https://github.com/arbrad/IC3ref
[2]
Bowen Alpern and Fred B Schneider. 1987. Recognizing safety and liveness. Distributed computing, 2, 3 (1987), 117–126. https://doi.org/10.1007/bf01782772
[3]
Patrick Behm, Paul Benoit, Alain Faivre, and Jean-Marc Meynadier. 1999. Météor: A Successful Application of B in a Large Project. In FM’99 — Formal Methods, Jeannette M. Wing, Jim Woodcock, and Jim Davies (Eds.). Springer Berlin Heidelberg, Berlin, Heidelberg. 369–387. isbn:978-3-540-48119-5
[4]
Yves Bertot and Pierre Castéran. 2013. Interactive theorem proving and program development: Coq’Art: the calculus of inductive constructions. Springer Science & Business Media.
[5]
Armin Biere. 2007. The AIGER and-inverter graph (AIG) format version 20071012.
[6]
Armin Biere, Alessandro Cimatti, Edmund M Clarke, Masahiro Fujita, and Yunshan Zhu. 1999. Symbolic model checking using SAT procedures instead of BDDs. In Proceedings of the 36th annual ACM/IEEE Design Automation Conference. 317–320.
[7]
Armin Biere, Alessandro Cimatti, Edmund M Clarke, Ofer Strichman, and Yunshan Zhu. [n. d.]. Bounded model checking. Handbook of satisfiability, 185, 99 ([n. d.]), 457–481.
[8]
Andrea Bonacchi, Alessandro Fantechi, Stefano Bacherini, Matteo Tempestini, and Leonardo Cipriani. 2014. Validation of Railway Interlocking Systems by Formal Verification, A Case Study. In Software Engineering and Formal Methods, Steve Counsell and Manuel Núñez (Eds.). Springer International Publishing, Cham. 237–252. isbn:978-3-319-05032-4
[9]
Arne Borälv. 2018. Interlocking Design Automation Using Prover Trident. In Formal Methods, Klaus Havelund, Jan Peleska, Bill Roscoe, and Erik de Vink (Eds.). Springer International Publishing, Cham. 653–656. isbn:978-3-319-95582-7
[10]
Aaron R Bradley. 2011. SAT-based model checking without unrolling. In International Workshop on Verification, Model Checking, and Abstract Interpretation. 70–87.
[11]
Simon Busard, Quentin Cappart, Christophe Limbrée, Charles Pecheur, and Pierre Schaus. 2015. Verification of railway interlocking systems. In ESSS.
[12]
Quentin Cappart, Christophe Limbrée, Pierre Schaus, and Axel Legay. 2015. Verification by discrete simulation of interlocking systems. In 29th Annual European Simulation and Modelling Conference. 402–409.
[13]
Quentin Cappart, Christophe Limbrée, Pierre Schaus, Jean Quilbeuf, Louis-Marie Traonouez, and Axel Legay. 2017. Verification of Interlocking Systems Using Statistical Model Checking. In 2017 IEEE 18th International Symposium on High Assurance Systems Engineering (HASE). 61–68. https://doi.org/10.1109/HASE.2017.10
[14]
Basri Tugcan Celebi and Ozgur Turay Kaymakci. 2016. Verifying the accuracy of interlocking tables for railway signalling systems using abstract state machines. Journal of Modern Transportation, 24 (2016), 277–283.
[15]
Yu Chen, Xiaoyu Zhang, and Jianwen Li. 2022. Finite Quantified Linear Temporal Logic and Its Satisfiability Checking. In Artificial Intelligence Logic and Applications: The 2nd International Conference, AILA 2022, Shanghai, China, August 26–28, 2022, Proceedings. 3–18.
[16]
A. Cimatti, E. Clarke, F. Giunchiglia, and M. Roveri. 2000. NUSMV: a new symbolic model checker. International Journal on Software Tools for Technology Transfer, 2, 4 (2000), 410–425.
[17]
Alessandro Cimatti and Alberto Griggio. 2012. Software model checking via IC3. In International Conference on Computer Aided Verification. 277–293.
[18]
Edmund M Clarke. 1997. Model checking. In International Conference on Foundations of Software Technology and Theoretical Computer Science. 54–56.
[19]
Dalay Israel de Almeida Pereira, David Deharbe, Matthieu Perin, and Philippe Bon. 2019. B-Specification of Relay-Based Railway Interlocking Systems Based on the Propositional Logic of the System State Evolution. In Reliability, Safety, and Security of Railway Systems. Modelling, Analysis, Verification, and Certification, Simon Collart-Dutilleul, Thierry Lecomte, and Alexander Romanovsky (Eds.). Springer International Publishing, Cham. 242–258. isbn:978-3-030-18744-6
[20]
Niklas Eén, Alan Mishchenko, and Robert Brayton. 2011. Efficient implementation of property directed reachability. In 2011 Formal Methods in Computer-Aided Design (FMCAD). 125–134.
[21]
BS EN. 2011. 50128 (2011). Railway Applications-Communication, Signalling and processing systems: Software for railway control and protection systems. International Electrotechnical Commission.
[22]
Alessio Ferrari, Gianluca Magnani, Daniele Grasso, and Alessandro Fantechi. 2011. Model checking interlocking control tables. In FORMS/FORMAT 2010. Springer, 107–115.
[23]
Alessio Ferrari, Maurice H. ter Beek, Franco Mazzanti, Davide Basile, Alessandro Fantechi, Stefania Gnesi, Andrea Piattino, and Daniele Trentini. 2019. Survey on Formal Methods and Tools in Railways: The ASTRail Approach. In Reliability, Safety, and Security of Railway Systems. Modelling, Analysis, Verification, and Certification, Simon Collart-Dutilleul, Thierry Lecomte, and Alexander Romanovsky (Eds.). Springer International Publishing, Cham. 226–241. isbn:978-3-030-18744-6
[24]
Giuseppe De Giacomo and Moshe Y. Vardi. 2013. Linear temporal logic and linear dynamic logic on finite traces. AAAI Press.
[25]
Giuseppe De Giacomo and Moshe Y. Vardi. 2015. Synthesis for LTL and LDL on finite traces. AAAI Press.
[26]
Tim Gonschorek, Ludwig Bedau, and Frank Ortmeier. 2018. Bringing formal methods on the rail. Safety and Reliability – Safe Societies in a Changing World.
[27]
Anne E. Haxthausen, Jan Peleska, and Ralf Pinger. 2014. Applied Bounded Model Checking for Interlocking System Designs. In Software Engineering and Formal Methods, Steve Counsell and Manuel Núñez (Eds.). Springer International Publishing, Cham. 205–220. isbn:978-3-319-05032-4
[28]
G. J. Holzmann. 1997. The Model Checker - SPIN. IEEE Transactions on Software Engineering, 23 (1997), 279–295.
[29]
Alexei Iliasov, Ilya Lopatkin, and Alexander Romanovsky. 2013. The SafeCap Platform for Modelling Railway Safety and Capacity. In Computer Safety, Reliability, and Security, Friedemann Bitsch, Jérémie Guiochet, and Mohamed Kaâniche (Eds.). Springer Berlin Heidelberg, Berlin, Heidelberg. 130–137. isbn:978-3-642-40793-2
[30]
Alexei Iliasov, Dominic Taylor, Linas Laibinis, and Alexander Romanovsky. 2018. Formal Verification of Signalling Programs with SafeCap. In Computer Safety, Reliability, and Security, Barbara Gallina, Amund Skavhaug, and Friedemann Bitsch (Eds.). Springer International Publishing, Cham. 91–106. isbn:978-3-319-99130-6
[31]
Alexei Iliasov, Dominic Taylor, Linas Laibinis, and Alexander Romanovsky. 2022. Practical Verification of Railway Signalling Programs. IEEE Transactions on Dependable and Secure Computing, 1–1. https://doi.org/10.1109/TDSC.2022.3141555
[32]
Alexander Ivrii and Arie Gurfinkel. 2015. Pushing to the top. In 2015 Formal Methods in Computer-Aided Design (FMCAD). 65–72.
[33]
Phillip James, Andy Lawrence, Faron Moller, Markus Roggenbach, Monika Seisenberger, Anton Setzer, Karim Kanso, and Simon Chadwick. 2014. Verification of Solid State Interlocking Programs. In Software Engineering and Formal Methods, Steve Counsell and Manuel Núñez (Eds.). Springer International Publishing, Cham. 253–268. isbn:978-3-319-05032-4
[34]
Andrew Lawrence, Monika Seisenberger, Andrew Lawrence, and Monika Seisenberger. 2010. Verification of railway interlockings in scade. In AVOCS’10, Proceedings of the 10th International Workshop on Automated Verification of Critical Systems and the Rodin User and Develop Workshop. Springer, 112–114.
[35]
Marie Le Bliguet and Andreas Andersen Kjæ r. 2008. Modelling interlocking systems for railway stations. Master’s thesis. Technical University of Denmark, DTU, DK-2800 Kgs. Lyngby, Denmark.
[36]
Michael Leuschel and Michael Butler. 2003. ProB: A model checker for B. In International symposium of formal methods europe. 855–874.
[37]
Jianwen Li, Rohit Dureja, Geguang Pu, Kristin Yvonne Rozier, and Moshe Y Vardi. 2018. Simplecar: An efficient bug-finding tool based on approximate reachability. In International Conference on Computer Aided Verification. 37–44.
[38]
Jianwen Li, Lijun Zhang, Geguang Pu, Moshe Y. Vardi, and Jifeng He. 2013. LTL Satisfiability Checking Revisited. In 2013 20th International Symposium on Temporal Representation and Reasoning (TIME).
[39]
J. Li, S. Zhu, G. Pu, and M. Vardi. 2015. SAT-based Explicit LTL Reasoning. Haifa Verification Conference.
[40]
Jianwen Li, Shufang Zhu, Yueling Zhang, Geguang Pu, and Moshe Y Vardi. 2017. Safety model checking with complementary approximations. In 2017 IEEE/ACM International Conference on Computer-Aided Design (ICCAD). 95–100.
[41]
Bidhan Malakar and B.K. Roy. 2014. Railway fail-safe signalization and interlocking design based on automation Petri Net. In International Conference on Information Communication and Embedded Systems (ICICES2014). 1–4. https://doi.org/10.1109/ICICES.2014.7034154
[42]
Ma Maofei and Zhang Yong. 2020. Modeling and Formal Verification of Interlocking System Based on UML and HCPN. In 2020 World Conference on Computing and Communication Technologies (WCCCT). 47–52. https://doi.org/10.1109/WCCCT49810.2020.9170006
[43]
Kenneth L McMillan. 2003. Interpolation and SAT-based model checking. In International Conference on Computer Aided Verification. 1–13.
[44]
T. Michaud and M. Colange. 2018. Reactive synthesis from LTL specification with Spot. In In Proceedings of the 7th Workshop on Synthesis.
[45]
Andrew Nash, Daniel Huerlimann, Jörg Schütte, and Vasco Paul Krauss. 2004. Railml† a standard data interface for railroad applications. WIT Transactions on The Built Environment, 74 (2004).
[46]
Kristin Y. Rozier and Moshe Y. Vardi. 2007. LTL Satisfiability Checking. In International SPIN Workshop on Model Checking of Software.
[47]
Yakir Vizel and Arie Gurfinkel. 2014. Interpolating property directed reachability. In International Conference on Computer Aided Verification. 260–276.
[48]
Linh Hong Vu, Anne E. Haxthausen, and Jan Peleska. 2017. Formal modelling and verification of interlocking systems featuring sequential release. Science of Computer Programming, 133 (2017), 91–115. issn:0167-6423 https://doi.org/10.1016/j.scico.2016.05.010 Formal Techniques for Safety-Critical Systems (FTSCS 2014)
[49]
Jim Woodcock, Peter Gorm Larsen, Juan Bicarregui, and John S. Fitzgerald. 2009. Formal methods: Practice and experience. ACM Comput. Surv., 41 (2009), 19:1–19:36.
[50]
W. Zhu. 2021. Big Data on Linear Temporal Logic Formulas. In 2021 IEEE 4th Advanced Information Management, Communicates, Electronic and Automation Control Conference (IMCEC).
Index Terms
- LightF3: A Lightweight Fully-Process Formal Framework for Automated Verifying Railway Interlocking Systems
Recommendations
Automated generation of formal safety conditions from railway interlocking tables
This paper describes a tool for extracting formal safety conditions from interlocking tables for railway interlocking systems. The tool has been applied to generate safety conditions for the interlocking system at Stenstrup station in Denmark, and the ...
Model checking railway interlocking systems
For supporting the analysis of railway interlocking systems in the early stage of their design we propose the use of model checking. We investigate the use of the formal modelling language CSP and the corresponding model checker FDR. In this paper, we ...
Model checking railway interlocking systems
ACSC '02: Proceedings of the twenty-fifth Australasian conference on Computer science - Volume 4For supporting the analysis of railway interlocking systems in the early stage of their design we propose the use of model checking. We investigate the use of the formal modelling language CSP and the corresponding model checker FDR. In this paper, we ...
Comments
Please enable JavaScript to view thecomments powered by Disqus.Information & Contributors
Information
Published In
November 2023
2215 pages
ISBN:9798400703270
DOI:10.1145/3611643
- General Chair:
- Satish Chandra,
- Program Chairs:
- Kelly Blincoe,
- Paolo Tonella
Copyright © 2023 ACM.
Permission to make digital or hard copies of all or part of this work for personal or classroom use is granted without fee provided that copies are not made or distributed for profit or commercial advantage and that copies bear this notice and the full citation on the first page. Copyrights for components of this work owned by others than the author(s) must be honored. Abstracting with credit is permitted. To copy otherwise, or republish, to post on servers or to redistribute to lists, requires prior specific permission and/or a fee. Request permissions from [email protected].
Sponsors
Publisher
Association for Computing Machinery
New York, NY, United States
Publication History
Published: 30 November 2023
Check for updates
Badges
Author Tags
Qualifiers
- Research-article
Conference
ESEC/FSE '23
Sponsor:
ESEC/FSE '23: 31st ACM Joint European Software Engineering Conference and Symposium on the Foundations of Software Engineering
December 3 - 9, 2023
CA, San Francisco, USA
Acceptance Rates
Overall Acceptance Rate 112 of 543 submissions, 21%
Contributors
Other Metrics
Bibliometrics & Citations
Bibliometrics
Article Metrics
- 0Total Citations
- 85Total Downloads
- Downloads (Last 12 months)85
- Downloads (Last 6 weeks)6
Reflects downloads up to 05 Nov 2024
Other Metrics
Citations
View Options
Get Access
Login options
Check if you have access through your login credentials or your institution to get full access on this article.
Sign in