Automated Parameterized Verification of a Railway Protection System with Dafny

In this paper we describe an industrial experience in the verification of the logic of a Railway Protection System (RPS). The RPS is designed within AIDA, a structured model-based design workflow and toolset. The RPS is written in a domain specific language amenable to signaling engineers, that is converted into Extended Finite State Machines (EFSM), and then into executable code. The RPS is parameterized, i.e., it can be applied, after configuration, in different operational scenarios. The logic is divided in classes, that are instantiated depending on the specific application. The verification challenge is to ensure that the required properties hold for all possible instantiations. We follow a verification approach based on the use of deductive methods, leveraging the Dafny framework. The AIDA environment is used to translate the RPS logic into Dafny, and also to automatically generate the contracts summarizing the methods implementing the guards and effects of the EFSM transitions. This approach greatly limits the need for human interaction with the underlying Dafny proof engine. In addition to domain specific optimizations, it results in an automated and efficient proof of the RPS properties.