European Train Control System: A Case Study in Formal Verification
European Train Control System: A Case Study in Formal Verification
复制标题
DOI：
10.1007/978-3-642-10373-5_13
复制
发表时间：
2009-11
期刊：
影响因子：
--
通讯作者：
André Platzer;Jan-David Quesel
中科院分区：
文献类型：
--
作者：
André Platzer;Jan-David Quesel
复杂的物理系统具有多个自由度。只有当它们的控制参数服从相应的约束时，它们才能正确工作。基于欧洲列车控制系统（ETCS）的非形式化规范，设计了一个用于其协作协议的控制器。对于其自由参数，我们依次确定所需的约束，以确保碰撞自由。我们正式证明的参数约束是尖锐的，他们等价的混合动力系统动力学的可达性方面的特征。使用我们的演绎验证工具KeYmaera，我们正式验证的ETCS协议，需要碰撞自由的可控性，安全性，活性和反应性属性。我们证明了ETCS协议仍然是正确的，即使在存在扰动的动态扰动。我们验证，安全性得到保护时，PI控制的速度监督使用。
Complex physical systems have several degrees of freedom. They only work correctly when their control parameters obey corresponding constraints. Based on the informal specification of theEuropean Train Control System(ETCS), we design a controller for its cooperation protocol. For its free parameters, we successively identify constraints that are required to ensure collision freedom. We formally prove the parameter constraints to be sharp by characterizing them equivalently in terms of reachability properties of the hybrid system dynamics. Using our deductive verification tool KeYmaera, we formally verify controllability, safety, liveness, and reactivity properties of the ETCS protocol that entail collision freedom. We prove that the ETCS protocol remains correct even in the presence of perturbation by disturbances in the dynamics. We verify that safety is preserved when a PI controlled speed supervision is used.