TY - GEN
T1 - Automated Compositional Verification of Interlocking Systems
AU - Haxthausen, Anne E.
AU - Fantechi, Alessandro
AU - Gori, Gloria
AU - Mikkelsen, Óli Kárason
AU - Petersen, Sofie Amalie
N1 - Publisher Copyright:
© 2023, The Author(s), under exclusive license to Springer Nature Switzerland AG.
PY - 2023
Y1 - 2023
N2 - Model checking techniques have often been applied to the verification of railway interlocking systems. However, these techniques may fail to scale to interlockings controlling large railway networks, composed by hundreds of controlled entities, due to the state space explosion problem. We have previously proposed a compositional method to reduce the size of networks to be model checked: the idea is to divide the network of the system to be verified into two sub-networks and then model check the model instances for these sub-networks instead of that for the full network. If given well-formedness conditions are satisfied by the network and the kind of division performed, it is proved that model checking safety properties of all such sub-networks guarantees safety properties of the full network. In this paper we observe that such a network division can be repeated, so that in the end, the full network has been divided into a number of sub-networks of minimal size, each being an instance of one of a limited set of “elementary networks”, for which safety proofs have easily been given by model checking once for all. The paper defines a division algorithm, and shows how, applying it to some examples of different complexity, a network can be automatically decomposed into a set of elementary networks, hence proving its safety. The execution time for such a verification turns out to be a very small fraction of the time needed for a model checker to verify safety of the full network.
AB - Model checking techniques have often been applied to the verification of railway interlocking systems. However, these techniques may fail to scale to interlockings controlling large railway networks, composed by hundreds of controlled entities, due to the state space explosion problem. We have previously proposed a compositional method to reduce the size of networks to be model checked: the idea is to divide the network of the system to be verified into two sub-networks and then model check the model instances for these sub-networks instead of that for the full network. If given well-formedness conditions are satisfied by the network and the kind of division performed, it is proved that model checking safety properties of all such sub-networks guarantees safety properties of the full network. In this paper we observe that such a network division can be repeated, so that in the end, the full network has been divided into a number of sub-networks of minimal size, each being an instance of one of a limited set of “elementary networks”, for which safety proofs have easily been given by model checking once for all. The paper defines a division algorithm, and shows how, applying it to some examples of different complexity, a network can be automatically decomposed into a set of elementary networks, hence proving its safety. The execution time for such a verification turns out to be a very small fraction of the time needed for a model checker to verify safety of the full network.
KW - Compositional Verification
KW - Formal Methods
KW - Interlocking Systems
KW - Model Checking
U2 - 10.1007/978-3-031-43366-5_9
DO - 10.1007/978-3-031-43366-5_9
M3 - Article in proceedings
AN - SCOPUS:85174435452
SN - 978-3-031-43365-8
T3 - Lecture Notes in Computer Science
SP - 146
EP - 164
BT - Proceedings of 5th International Conference Reliability, Safety, and Security of Railway Systems
PB - Springer
T2 - 5<sup>th</sup> International conference on Reliability, Safety and Security of Railway Systems
Y2 - 10 October 2023 through 12 October 2023
ER -