Halfway Generic Verification of Railway Control Systems

Halfway Generic Verification of Railway Control Systems

연구 분야: Verification

학회: International Conference on Reliability, Safety, and Security of Railway Systems

Formal verification of railway control systems, particularly Generic Applications (GAs) and Specific Applications (SAs), is crucial due to their complexity and safety-critical nature. This paper presents a novel framework, Halfway Generic Verification (HGV), applying Software Product Line (SPL) principles for formal verification of railway control systems. The HGV method offers a balanced approach that can verify a broad set of systems derived from the same Generic Design Specification (GDS) in a single computational sweep, retaining feasibility. It also highlights the potential benefits of implementing SPL analysis in modeling and verification of railway control systems, which include enhancing the process of configuration data generation and ensuring the correctness of the GDS and Generic Safety Specification. The effectiveness of the HGV approach is demonstrated with a prototype implementation utilizing the Prover iLock tool.