Verification of the European Rail Traffic Management System in Real-Time Maude
Verification of the European Rail Traffic Management System in Real-Time Maude
复制标题
DOI：
10.1016/j.scico.2017.10.011
复制
发表时间：
2018-03-01
影响因子：
1.3
通讯作者：
Seisenberger, Monika
中科院分区：
文献类型：
--
作者：
Berger, Ulrich;James, Phillip;Seisenberger, Monika
欧洲铁路交通管理系统 (ERTMS) 是一种最先进的列车控制系统，旨在作为欧洲铁路的标准。它将传统的离散联锁系统推广到一个世界，其中列车拥有用于信号传输的车载设备，并且列车和联锁通过无线电块处理器进行通信。 ERTMS 旨在提高轨道交通系统的性能和容量，同时不影响其安全性。ERTMS 系统具有混合性质，与仅处理离散数据的经典铁路信号系统不同。因此，转向 ERTMS 向正式方法界提出了许多研究问题，其中最突出的是：如何保证安全？在本文中，我们提出了 ERTMS 的第一个正式建模，其中包括参与其控制周期的所有子系统。我们从物理和逻辑角度理解了安全的含义，并证明了通过考虑大量双向轨道布局，利用实时莫德模型检查来证明 ERTMS 系统的安全性是可行的。ERTMS 目前已在许多国家安装。在可预见的将来，它将成为主要的列车控制标准。本文提出的概念提供了支持可靠 ERTMS 系统设计的适用方法。我们证明模型检查是分析大型复杂实时系统的可行选择。此外，我们建立了实时莫德作为适用于铁路领域的建模和验证工具。本文给出的方法是严格的。为了避免建模错误，我们遵循系统方法：首先，作为需求规范，我们识别 ERTMS 中存在的事件响应结构。然后，我们以可追溯的方式在 Real-Time Maude 中对这些结构进行建模，即 Real-Time Maude 中的规范文本可以直接映射到需求。我们通过检查模型是否具有所需的行为来探索我们的模型，并通过错误注入应用系统的模型探索 - 这两个步骤都是使用正式方法 Real-Time Maude 来执行的。最后，我们通过模型检验对ERTMS进行了分析，从而将形式化方法应用于铁路领域，并从数学上证明了我们对ERTMS的模型检验分析是完整的，即它始终保证安全。 (C) 2017 Elsevier B.V. 保留所有权利。
The European Rail Traffic Management System (ERTMS) is a state-of-the-art train control system designed as a standard for railways across Europe. It generalises traditional discrete interlocking systems to a world in which trains hold on-board equipment for signalling, and trains and interlockings communicate via radio block processors. The ERTMS aims at improving performance and capacity of rail traffic systems without compromising their safety.The ERTMS system is of hybrid nature, in contrast to classical railway signalling systems which deal with discrete data only. Consequently, the switch to ERTMS poses a number of research questions to the formal methods community, most prominently: How can safety be guaranteed? In this paper we present the first formal modelling of ERTMS comprising all subsystems participating in its control cycle. We capture what safety means in physical and in logical terms, and we demonstrate that it is feasible to prove safety of ERTMS systems utilising Real-Time Maude model-checking by considering a number of bi-directional track layouts.ERTMS is currently being installed in many countries. It will be the main train control standard for the foreseeable future. The concepts presented in this paper offer applicable methods supporting the design of dependable ERTMS systems. We demonstrate model checking to be a viable option in the analysis of large and complex real-time systems. Furthermore, we establish Real-Time Maude as a modelling and verification tool applicable to the railway domain.The approach given in this paper is a rigorous one. In order to avoid modelling errors, we follow a systematic approach: First, as a requirement specification, we identify the event-response structures present in the ERTMS. Then, we model these structures in Real-Time Maude in a traceable way, i.e., specification text in Real-Time Maude can be directly mapped to requirements. We explore our models by checking if they have the desired behaviour, and apply systematic model-exploration through error injection - both these steps are carried out using the formal method Real-Time Maude. Finally, we analyse ERTMS by model-checking, thus applying a formal method to the railway domain, and we mathematically prove that our analysis of ERTMS by model-checking is complete, i.e., that it guarantees safety at all times. (C) 2017 Elsevier B.V. All rights reserved.