Formal Analysis of a Railway Signaling Block Designed in AIDA

Ensuring the correctness of control logic in railway systems is essential for safety and reliability. In this paper, we present an industrial case study on the formal verification of a software component responsible for managing signal color aspects in a railway interlocking system. We work within AIDA, a model-based design environment where generic control logics are specified in a controlled natural language, and which then drives the automatic generation of SysML models and executable code. In the first phase, we followed an approach based on the use of the Dafny prover, analyzing the model automatically generated from AIDA. This model includes both the Dafny counterpart of the control logics and its annotations. When Dafny failed to prove the expected properties, manual inspection highlighted the existence of some corner cases that led to the discovery of actual bugs. After revising the logic, Dafny still failed to prove the overall correctness. Hence, we replaced manual inspection with the model checking of a carefully reduced model, obtained by localization reduction and focusing on the most relevant classes and havoc-ing the behavior of the others. The model was derived from the summarizations of the methods in Dafny, and could be fully analyzed with the nuXmv model checker. The subsequent automated analysis was able to detect additional violations, and to pinpoint them in the form of easy-to-understand counterexample traces (instead of returning a failed to prove answer).