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

该项目的总体目标是开发建模技术和工具，以提高铁路能力，同时确保保持安全标准。铁路领域已被确定为计算机科学的一个巨大挑战。由于其安全关键的性质，各种形式化的方法已被应用在这一领域，其中，最突出的是，B方法已成功地用于验证几条线路，包括那些在巴黎和圣胡安地铁。然而，大多数方法只关注安全，忽略了时间方面。此外，严格的时间处理本身就被计算机科学界广泛认为是一项挑战。然而，铁路网络节点的容量高度依赖于时间：移动一个点或一列火车通过一个节点需要时间，而瞄准和制动距离是时间的函数。这就是为什么我们建议扩展事件-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）在整个项目过程中，我们的工业合作伙伴英维思铁路公司将为项目团队提供轨道规划和控制软件，并将其用作案例研究，以便用真实的数据集挑战我们的方法。英维思铁路的定期会议和研讨会将提供必要的实际反馈，以提出铁路行业可行的解决方案。英维思铁路公司通过使用更智能的控制解决方案来提高地铁能力的成功经验将为这项工作做出宝贵的贡献。该项目的结果将用于评估提高铁路能力的方法的可行性，并为在铁路行业部署开发的解决方案做好准备。

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.