Theories, techniques and tools for engineering

铁路网络使用一系列不同的信号原理，例如基于路线的信号、速度信号、使用列车保护系统的信号，例如不同级别的欧洲列车控制系统，以及基于通信的列车控制。成本和实际限制意味着，每个网络在给定时间段内可以从一个系统更改到另一个系统的数量是有限的，因此网络不可避免地使用混合信令系统。对于这种混合系统的严格分析和模拟，没有单一的理论，这导致对工程判断的强烈依赖。这有可能导致过度设计或意外限制容量。在最坏的情况下，可能会遗漏某些有可能降低安全水平的情况。这项博士研究将发展这样的理论，用于建模和验证由混合信令区域组成的复杂网络。总体目标是提出一个通用的、开放的和可扩展的基于代理的框架，以能够捕获任何类型的信令，无论是传统的还是新的，这些理论将为系统安全性的全自动化验证提供正式的基础，可以使用先进的机械化定理证明来支持。作为研究的重要部分，我们还将开发技术来支持对异构系统能力的评估。研究将集中于通过一套具有特定领域接口且可扩展和使用的工具来支持此类理论的应用。这项工作将由行业需求驱动，并与西门子铁路自动化(Chippenham)密切合作，以确保结果具有在实际工业环境中部署的潜力。

Railway networks use a range of different signalling principles, for example route-based signalling, speed signalling, signalling using train protection systems such as the different levels of the European Train Control System, and Communication Based Train Control. Cost and practical constraints mean that there is a limit to the amount of each network that can be changed from one system to another in a given time period, as a result of which it is inevitable that networks use a mixture of signalling systems.There is no single theory for rigorous analysis and simulation of such mixed systems, leading to a strong dependence on engineering judgement. This has the potential to lead to either over-design or accidental restrictions in capacity. In the worst case certain situations which have the potential to reduce safety levels may be missed. The PhD study will develop such theories for modelling and verifying complex networks comprising areas with mixed signalling. The general aim is to come up with a general, open and extendable agent-based framework to enable capturing any type of signalling, legacy or new, and to assist signalling engineers in ensuring safety of such heterogeneous systems.The theories will provide a formal foundation for fully automated verification of system safety that can be tool supported with the use of the advanced mechanised theorem proving.As an important part of the study we will also develop techniques to support evaluation of heterogeneous systems' capacity.The study will focus on supporting the application of such theories by a set of tools that have domain-specific interfaces and are scalable and useable.The work will be driven by the needs of industry and conducted in a close cooperation with Siemens Rail Automation (Chippenham) to ensure that the results have potential to be deployed in real industrial settings.