Interlocking logics are at the core of critical systems controlling the traffic within stations. In this paper, we consider a generic interlocking logic, which can be instantiated to control a wide class of stations. We tackle the problem of parameterized verification, i.e. prove that the logic satisfies the required properties for all the relevant stations. We present a simplified case study, where the interlocking logic is directly encoded in Dafny. Then, we show how to automate the proof of an important safety requirement, by integrating simple, template-based invariants and more complex invariants obtained from a model checker for parameterized systems. Based on these positive preliminary results, we outline how we intend to integrate the approach by extending the IDE for the design of the interlocking logic.

翻译：联锁逻辑是控制站场内交通的关键系统的核心。本文考虑一种可实例化以控制广泛站场类别的通用联锁逻辑。我们着手解决参数化验证问题，即证明该逻辑对所有相关站场均满足所需属性。我们展示了一个简化案例研究，其中联锁逻辑直接以Dafny编码。随后，我们展示了如何通过整合基于模板的简单不变量与从参数化系统模型检验器获得的更复杂不变量，来自动化一项关键安全需求的证明。基于这些积极的初步结果，我们概述了通过扩展用于联锁逻辑设计的集成开发环境来整合该方法的计划。