Formal Verification of Interlocking Systems

June.2022 – June.2023 Supervised by Jianwen Li and Geguang Pu from ECNU.

See: Talk, Demo,Bench, Paper

The formal verification of interlocking systems has long been an open problem due to the complexity of domain knowledge.

With the help of our industrial partner, I designed a Domain Specific Language RIS-FL and implemented LightF3, a formal framework for verifying railway interlocking systems and evaluated it with real station instances from our industrial partner, demonstrating its effectiveness. With its help, we successfully found deep hidden bugs in existing designs.

Our paper was accepted by FSE’23 (The ACM International Conference on the Foundations of Software Engineering).