Efficient verification of railway infrastructure designs against standard regulations
Efficient verification of railway infrastructure designs against standard regulations
复制标题
根据标准法规有效验证铁路基础设施设计
DOI：
--
复制
发表时间：
2018
期刊：
影响因子：
--
通讯作者：
Christian Johansen
中科院分区：
文献类型：
--
作者：
Bjørnar Luteberget;Christian Johansen
在设计安全关键基础设施方面，S.A.在铁路系统中，工程师经常要处理复杂和大规模的设计。形式化方法可以在帮助自动化各种任务方面发挥重要作用。对于铁路设计，形式化的方法主要用于通过模型检验来验证所谓的错位的安全性，该方法处理状态变化和相当复杂的属性，通常会导致相当大的计算负担(例如，状态空间爆炸问题)。相比之下，我们专注于静态基础设施模型，并对检查来自设计指导方针和法规的要求感兴趣，这些要求通常由铁路当局或安全认证机构给出。我们的目标是通过使用速度足够快的软件进行即时验证，使铁路工程师在确保遵守法规时所做的繁琐手工工作自动化，从而能够包括在铁路设计工具中，就像IDE中的编译器一样。因此，本文描述了将形式化方法集成到铁路设计过程中，以自动从CAD铁路设计中提取铁路模型，并将相关的技术法规和专家知识描述为模型上要检查的属性。我们采用了Datalog的一种变体，并使用标准化的铁路标记语言RARML作为形式化的基础和交换格式。我们开发了一个原型工具，并将其集成到工业铁路CAD软件中，该软件以RailCOMPLETE®为名称开发。这个即时验证工具是工程师在进行设计时的帮助，但不能替代其他更重的软件，如进行联锁验证或容量分析。我们的工具，通过导出到RARML，可以很容易地与这些其他工具集成。我们将我们的工具链应用于挪威铁路项目--阿尔纳火车站的升级改造。
In designing safety-critical infrastructures s.a. railway systems, engineers often have to deal with complex and large-scale designs. Formal methods can play an important role in helping automate various tasks. For railway designs formal methods have mainly been used to verify the safety of so-called interlockings through model checking, which deals with state change and rather complex properties, usually incurring considerable computational burden (e.g., the state-space explosion problem). In contrast, we focus on static infrastructure models, and are interested in checking requirements coming from design guidelines and regulations, as usually given by railway authorities or safety certification bodies. Our goal is to automate the tedious manual work that railway engineers do when ensuring compliance with regulations, through using software that is fast enough to do verification on-the-fly, thus being able to be included in the railway design tools, much like a compiler in an IDE. In consequence, this paper describes the integration into the railway design process of formal methods for automatically extracting railway models from the CAD railway designs and for describing relevant technical regulations and expert knowledge as properties to be checked on the models. We employ a variant of Datalog and use the standardized “railway markup language” railML as basis and exchange format for the formalization. We developed a prototype tool and integrated it in industrial railway CAD software, developed under the name RailCOMPLETE®. This on-the-fly verification tool is a help for the engineer while doing the designs, and is not a replacement to other more heavy-weight software like for doing interlocking verification or capacity analysis. Our tool, through the export into railML, can be easily integrated with these other tools. We apply our tool chain in a Norwegian railway project, the upgrade of the Arna railway station.
工业关键系统的形式化方法
DOI：
10.1007/978-3-642-04570-7_1
发表时间：
2009
期刊：
--
影响因子：
--
作者：
Distefano D
通讯作者：
Distefano D