Overcoming the railway capacity challenges without undermining rail network safety (SafeCap)

在不损害铁路网络安全的情况下克服铁路容量挑战（SafeCap）

• 批准号: EP/I010807/1
• 负责人: Alexander Romanovsky
• 金额: $ 47.06万
• 依托单位: Newcastle University
• 依托单位国家: 英国
• 项目类别: Research Grant
• 财政年份: 2011
• 资助国家: 英国
• 起止时间: 2011 至 无数据
• 项目状态: 已结题
• 来源: https://gtr.ukri.org/projects?ref=EP%2FI010807%2F1
• 关键词: Overcoming; railway; capacity; challenges; without

The overall aim of this project is to develop modelling techniques and tools for improving railway capacity while ensuring that safety standards are maintained.The railway domain has been identified as a grand challenge for computer science. Due to its safety-critical nature, various formal methods have been applied in this domain, where, most prominently, the B method has been successfully used to verify several lines, including those in Paris and San Juan Metro. Solely concerned with safety, most approaches have, however, ignored the aspect of time. Furthermore, a rigorous treatment of time is widely recognised as a challenge in its own right by the computer science community.And yet the capacity of a rail network node is highly dependent on time: moving a point or a train through a node takes time, and sighting and braking distances are functions of time. This is why we propose extending Event-B, a modern variant of the B method, with reasoning about time and underpinning it with various tools for simulation, analysis and verification. To this end, we will integrate Event-B with process algebra CSP. This will make it possible to re-use proof support developed for CSP. Overall, our approach will allow an integrated view of rail networks, within which capacity can be investigated without compromising safety.In our project, we will handle time precisely, i.e. without any rounding errors. In simulations, this can be achieved by using the rationals in the language Haskell; in proofs, the theorem prover Isabelle/HOL includes proper real numbers (as well as rationals). We will extend the interactive proof tool CSP-Prover and build a new tool support. By relying on such tool support, the railway engineer will be able to model and evaluate the impact on capacity of altering track layouts, signalling principles, driving rules and control algorithms. By integrating our tool into the Event-B tool environment, our project will deliver a software development platform that would allow engineers to model, simulate, analyse and verify railway network nodes (both junctions and stations) in an integrated way, combining reasoning about capacity and safety.To achieve our overall aim of improving railway capacity, we intend to meet the following technological (T) and scientific (S) and objectives:1) To integrate proof-based reasoning about time in state-based models, exemplified by Event-B and CSP-Prover, and to provide an open tool support for verifying timed systems (S).2) To develop an intuitive graphical domain-specific language for the railway domain with a tailored tool support based on the Rodin framework (T)3) To identify and validate design patterns for improving capacity by altering route design, track layout, signalling principles and driving rules (T)Throughout the project, our industrial partner Invensys Rail will provide the project team with track plans and control software, which will be used as case studies in order to challenge our approach with realistic data sets. Regular meetings and workshops involving Invensys Rail will give the practical feedback necessary to come up with solutions which are viable for the rail industry. Invensys Rail's successful experience of improving the capacity of metro railways by using smarter control solutions will be an invaluable contribution to this work.The results of the project will be used to evaluate the viability of approaches to improving railway capacity and to prepare the deployment of the developed solutions in the railway industry.

该项目的总体目标是开发建模技术和工具，以提高铁路容量，同时确保维持安全标准。铁路领域已被认为是计算机科学的巨大挑战。由于其安全性至关重要，该领域已应用各种形式化方法，其中最突出的是，B 方法已成功用于验证多条线路，包括巴黎和圣胡安地铁的线路。然而，大多数方法仅考虑安全性，而忽略了时间方面。此外，计算机科学界广泛认为对时间的严格处理本身就是一个挑战。然而，铁路网络节点的容量高度依赖于时间：移动一个点或一列火车通过一个节点需要时间，而瞄准和制动距离是时间的函数。这就是为什么我们建议扩展 Event-B（B 方法的现代变体），对时间进行推理，并使用各种模拟、分析和验证工具来支撑它。为此，我们将 Event-B 与流程代数 CSP 集成。这将使重用为 CSP 开发的证明支持成为可能。总的来说，我们的方法将允许对铁路网络进行综合视图，在不影响安全性的情况下可以调查容量。在我们的项目中，我们将精确地处理时间，即没有任何舍入误差。在模拟中，这可以通过使用 Haskell 语言中的有理数来实现；在证明中，定理证明者 Isabelle/HOL 包括真实数（以及有理数）。我们将扩展交互式证明工具CSP-Prover并构建新的工具支持。依靠此类工具支持，铁路工程师将能够建模并评估改变轨道布局、信号原理、驾驶规则和控制算法对容量的影响。通过将我们的工具集成到Event-B工具环境中，我们的项目将提供一个软件开发平台，使工程师能够以集成的方式对铁路网络节点（交叉口和车站）进行建模、模拟、分析和验证，结合容量和安全的推理。为了实现提高铁路容量的总体目标，我们打算满足以下技术（T）和科学（S）和目标：1）在基于状态的模型中集成关于时间的基于证据的推理， 以 Event-B 和 CSP-Prover 为例，并为验证定时系统提供开放工具支持 (S)。2) 通过基于 Rodin 框架的定制工具支持，为铁路领域开发直观的图形领域特定语言 (T)3) 识别和验证设计模式，通过改变路线设计、轨道布局、信号原理和驾驶规则来提高容量 (T)在整个项目中，我们的工业合作伙伴英维思铁路将提供 项目团队拥有跟踪计划和控制软件，这些软件将用作案例研究，以便用实际数据集挑战我们的方法。涉及英维思铁路的定期会议和研讨会将提供必要的实际反馈，以提出对铁路行业可行的解决方案。英维思铁路通过使用更智能的控制解决方案提高地铁铁路运力的成功经验将为这项工作做出宝贵的贡献。该项目的结果将用于评估提高铁路运力的方法的可行性，并为在铁路行业部署已开发的解决方案做好准备。

项目成果

Integrated Formal Methods

综合形式化方法

• DOI: 10.1007/978-3-319-33693-0_8
• 发表时间: 2016
• 作者: Andrei O

Developing a well-received pre-matriculation program: the evolution of MedFIT.

制定广受好评的预科课程：MedFIT 的演变。

• DOI: 10.1007/978-3-319-11970-0_12
• 发表时间: 2022
• 期刊: Discover education
• 作者: Allen A

Techniques for modelling and verifying railway interlockings

• DOI: 10.1007/s10009-014-0304-7
• 发表时间: 2014-11
• 期刊: International Journal on Software Tools for Technology Transfer
• 影响因子: 1.5
• 作者: Phillip James;F. Moller;N. H. Nga;M. Roggenbach;Steve A. Schneider;H. Treharne

A Simulator for Timed CSP

定时 CSP 模拟器

• 作者: Markus Roggenbach (Co-Author)

The SafeCap toolset for improving railway capacity while ensuring its safety.

SafeCap 工具集用于提高铁路容量，同时确保其安全。

• 作者: Alexander Romanovsky (Author)