一句话：提出 LightF3 框架，以基于 FQLTL 的 RIS-FL 语言建模联锁系统并自动转换为 AIGER，调用主流模型检测器完成验证。
铁路联锁系统是整个信号系统安全的基础，其功能正确性至关重要。已有形式化建模与验证工作存在两个突出问题：一是建模多复用通用模型，造成过度泛化，未能利用联锁系统的固有特性；二是验证技术难以与时俱进，缺乏集成最新验证算法与工具的可适配途径。为此，作者提出 LightF3——一个轻量级、全流程的联锁系统形式化建模与验证框架。LightF3 定义 RIS-FL 语言，基于 FQLTL（LTL 的一种变体）描述系统模型与规约；随后自动将 RIS-FL 模型转换为 AIGER 格式，即当前主流模型检测器的输入格式，并调用最先进的检测器完成验证任务。作者在工业合作方提供的五个真实车站实例上进行了评估，验证了该框架的有效性，并统计分析了不同模型检测技术的验证结果，为铁路联锁与形式化方法社区提供了有益结论。
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.
@inproceedings{DongZXCCMLP23,
title = {LightF3: A Lightweight Fully-Process Formal Framework for Automated Verifying Railway Interlocking Systems},
author = {Yibo Dong and Xiaoyu Zhang and Yicong Xu and Chang Cai and Yu Chen and Weikai Miao and Jianwen Li and Geguang Pu},
booktitle = {FSE},
year = {2023},
doi = {10.1145/3611643.3613874}
}