Testing from verified test-models for ERMTS level 2

使用经过验证的 EMTS 2 级测试模型进行测试

• 批准号: 2122737
• 金额: --
• 依托单位: Swansea University
• 依托单位国家: 英国
• 项目类别: Studentship
• 财政年份: 2018
• 资助国家: 英国
• 起止时间: 2018 至 无数据
• 项目状态: 已结题
• 来源: https://gtr.ukri.org/projects?ref=studentship-2122737
• 关键词: Testing; verified; test; models; ERMTS

The ERTMS Train Control System is a state-of-the-art system designedas a standard for railways across Europe. While the ERTMS standarddetails the interactions between trains and track equipment (e.g., inorder to obtain concise train position information) and a radio blockcentre and trains (e.g., to hand out movement authorities), thedetails of how the controller, the interlocking and the radio blockcentre interact with each other are left to the suppliers ofsignalling solutions.Over the last four years, Siemens Rail Automation UK and SwanseaUniversity have co-operated on the development of a formal model ofERTMS level 2 as realised by Siemens. To the best of our knowledge,this work presents the first and currently only formal ERTMS modelthat encompasses all of the ERTMS subsystems required for the fullcontrol cycle. The model either provides a formal argument that agiven detailed design is safe, or it gives a counter example traceillustrating a sequence of events that leads to an unsafe situation.ObjectivesThis PhD project sets out to achieve the following objectives:Given a location-specific design for an ERMTS-controlled rail yard,i.e., interlocking tables and rules as to what messages the radioblock centre (RBC) shall send in different situations:[O1] to provide for this design a formally verified,location-specific test model;[O2] to derive test suites from this test model with which thelocation-specific Siemens RBC realisation and/or the location-specificinterlocking computer can be tested - either in isolation or incombination with each other.Time permitting, the last phase of the project could be on scoping how to extend this work to ERTMS level.Potential applications and benefits Railways in the UK - and worldwide - are experiencing ever moreintensive use of their services, as the demand for rail transportmodes increases. As this happens, the existing railway infrastructureis becoming more and more overloaded. Because of this, the problem ofincreasing the capacity of the nation's rail system is becoming asignificant challenge in the UK as well as elsewhere.One straightforward way to increase railway capacity is to simplybuild more railway tracks; e.g., High Speed Two (HS2) and Crossrailprovide two such high-profile solutions, the former for mainline railnetwork and the latter for London metro. However, this is a veryexpensive solution which is typically faced with insurmountableobstacles, such as the mere lack of space and the presence of listedbuildings. What is really needed, then, are ways to increase thecapacity of the existing rail network. To this end, upgradingsignalling and train control systems is regarded as a cost efficientway to increase the capacity in existing railway - and at the sametime decrease energy consumption.The European Train Control System of the European Rail TrafficManagement System (ERTMS-ETCS) has been proposed to do just this:classical traffic light signalling is replaced by communicationbetween a central unit and the trains. This project sets out toimprove quality assurance for ERTMS-ETCS by the use of formalmethods. When completed, this PhD project will contribute to Siemens RailUK quality assurance processes and bring benefits in terms of quality,time and cost. Beyond Siemens Rail UK, this could lead to a culturechange within the railway industry, in particular with respect tostandards and contracts for development. Furthermore, there is hopefor a wider societal impact concerning adaption of formal methods.Alignment to EPSRC research areasThis PhD project directly addresses two out of the four themes set outby EPSRC in their vision ""Science for a successful nation"":""Productive nation"", as the proposal directly reacts to research needsfrom Siemens Rail UK; and ""Resilient nation"" as it explicitly refersto the smooth a

ERTMS列车控制系统是一种最先进的系统，被设计为整个欧洲铁路的标准。虽然ERTMS标准详细说明了列车和轨道设备之间的相互作用(例如，为了获得简明的列车位置信息)以及无线电闭塞中心和列车之间的相互作用(例如，发放移动授权)，但控制器、联锁和无线电闭塞中心如何相互作用的细节留给了信号解决方案供应商。在过去的四年里，西门子英国铁路自动化公司和斯旺西大学合作开发了由西门子实现的ERTMS Level 2的正式模型。据我们所知，这项工作提出了第一个也是目前唯一一个正式的ERTMS模型，该模型涵盖了FullControl周期所需的所有ERTMS子系统。该模型提供了一个正式的论点，即即使是详细设计也是安全的，或者它给出了一个反例踪迹，说明了导致不安全情况的一系列事件。目标本博士项目旨在实现以下目标：给出ERMTS控制的铁路站场的特定位置设计，即联锁表和关于无线闭锁中心(RBC)在不同情况下应发送什么信息的规则：[O1]为该设计提供正式验证的特定位置测试模型；[O2]从该测试模型派生测试套件，使用该测试套件可以单独或结合测试特定位置的西门子RBC实现和/或特定位置的联锁计算机。如果时间允许，项目的最后阶段可能是研究如何将这项工作扩展到ERTMS级别。随着对铁路运输方式的需求增加，英国和世界各地的潜在应用和好处铁路正在经历其服务的日益密集的使用。随着这种情况的发生，现有的铁路基础设施正变得越来越超载。正因为如此，在英国和其他地方，提高国家铁路系统的运力正成为一个巨大的挑战。增加铁路运力的一个直接方法是简单地修建更多的铁轨；例如，高速二号(HS2)和Crossail提供了两个这样的备受瞩目的解决方案，前者用于主线铁路网，后者用于伦敦地铁。然而，这是一个非常昂贵的解决方案，通常面临着不可逾越的障碍，例如仅仅是缺乏空间和存在列出的建筑物。那么，真正需要的是增加现有铁路网运力的方法。为此，升级信号和列车控制系统被认为是增加现有铁路运力同时降低能源消耗的一种经济有效的方法。欧洲铁路交通管理系统的欧洲列车控制系统(ERTMS-ETCS)已被提出：用中央单元与列车之间的通信来取代传统的红绿灯信号。该项目旨在通过使用正式方法来提高ERTMS-ETCS的质量保证。该博士项目建成后，将为西门子英国铁路公司的质量保证流程做出贡献，并在质量、时间和成本方面带来好处。除了西门子英国铁路，这可能会导致铁路行业内的CULTURECHANGE，特别是在开发标准和合同方面。此外，正式方法的采用也有希望产生更广泛的社会影响。与EPSRC研究领域的结盟这个博士项目直接涉及EPSRC在其愿景中提出的四个主题中的两个：“科学造就一个成功的国家”：“多产的国家”，因为该提议直接回应了西门子英国铁路公司的研究需求；以及“弹性国家”，因为它明确地提到了