专业知识

开启探索之旅,了解联锁设计自动化和形式化的方法

研究报告

2021-07-01T09:14:22+01:00

研究报告-Prover iLock 流程

Prover iLock 是一个工具链,它可以实现计算机联锁系统的软件开发的自动化。新的 CENELEC SIL-4 认证的联锁系统能够在几天内生产出来,进而节省了大量的开发资源。

2021-07-01T09:24:33+01:00

联锁设计自动化的商业案例

本文旨在帮助负责开发铁路控制系统的供应商和项目运营商,如何在投资现代联锁设计自动化的过程中,创建成功的商业案例。我们还将介绍基于形式化规范和自动化工具的最先进流程。

视频资料

HLL 论坛 – HLL 使用者的社区

HLL 论坛是一个形式化规范语言 HLL的使用者的社区,我们相信它是形式化方法的上佳语言选择。并且随着它开始成为事实上的标准,我们希望确保该语言以可控的方式发展以满足未来的需求。

查看更多

专业词汇表

ATC

列车自动控制系统(ATC)是一种综合信号系统,可保证列车的安全运行。 ATC 集成了各种位于车上和地面的子系统。除了全部的联锁系统外,完整的 ATC 系统还包括三个子系统:(i) ATP、(ii) ATO 和 (iii) ATS。

ATO

自动列车操作系统(ATO)是一个 ATC 子系统,它执行通常由列车司机执行的车载非关键功能,包括确保列车平稳加速到运行速度,速度调节,以及平稳地将列车停靠在站台或停车信号前的适当位置。 ATO 子系统主要为机载,并且是无人驾驶系统中的主要组件之一。此外,ATO 子系统还会向中央控制室报告车辆健康状况。

ATP

列车自动防护系统(ATP)是负责信号系统安全运行的 ATC 子系统。它会对列车施加速度限制,以保持它们之间的安全运行距离,以及保证遵守安全和速度要求。 ATP 系统被设计为一个故障-安全(苛求)系统。

ATS
列车自动监控系统 (ATS) 是一个 ATC 子系统,它根据铁路时刻表通过 ATO 和 ATP 自动控制列车。 它还涉及到一个CTC系统。
Balise
地上应答器,它是放置在铁路轨道之间的电子信标或转发器,作为列车自动保护系统的一部分。
CBI

计算机联锁系统(CBI) 是一种联锁系统,传统的有线继电器网络被运行在具有特定目的的故障-安全控制硬件上的软件逻辑所取代。 该逻辑由软件而不是硬接线电路实现,这一改变极大地促进了必要时通过重新编程,而不是重新布线进行修改的能力。

CBTC

基于通信的列车自动控制系统(CBTC)是一个正在开发的系统,它将实现在各种地铁线路上使用的不同技术系统的互换性。 CBTC 可以理解为尝试为公共交通行业创建 ERTMS 类型的标准。

CENELEC

欧洲电工标准化委员会。

Completeness

完整性,如果系统中的每个有效公式都可以证明,则称该形式化系统是完备的。

CTC
调度集中控制系统(CTC)监控线路或网络上的信号状态,并将相关状态信息输出给中央操作工作人员,该操作员协助管理确保线路或网络情况与时间表一致,并操作控制以防止小的流程干扰导致交通拥堵。调度集中控制系统还会通知操作员列车自动控制系统的设备故障,以及动力牵引和客运站支持设备的故障。
Domain-Specific Language/DSL

领域特定语言/DSL,一种用于特定应用领域的编程语言。这与广泛适用于各个领域的通用语言 (GPL) 形成对比。 DSL 种类繁多,从广泛用于公共领域的语言(如用于网页的 HTML)到用于铁路系统中对象之间数据交换的铁路特定应用语言 RailML。 PiSPEC 是用于联锁系统规范的 DSL。

DRIMS

动态铁路信息管理系统

ERA

欧盟铁路局。

ERTMS

欧洲铁路管理系统,欧洲铁路交通管理系统 (ERTMS) 于 1992 年由欧盟引入,旨在创建统一的铁路交通指挥、控制和协调系统,以实现整个欧盟领土的“互操作性”。 ERTMS 标准存在三个级别(ERTMS 1、2 和 3),具体取决于用途,每个级别根据所使用的轨旁和车载设备的类型以及该设备传递相关数据的方式进行区分。

ETCS

欧洲列车控制系统 (ETCS) 是一种信号、控制和列车保护系统,旨在取代欧洲铁路目前使用的许多不兼容的安全系统(尤其是在高速线路上)。

EULYNX

欧洲创始连接联锁次系统

Finite state machine/FSM

有限状态机(FSM)是一种抽象机器,它在任意时刻都处于有限状态集合中的某一状态,并且可以响应某些外部输入,从一种状态变为另一种状态。 从一种状态到另一种状态的变化称为转换。

Formal methods

形式化方法,它是一种用于软件和硬件系统的描述、开发和验证的数学技术。

Formal specification

形式化描述,它是以定义明确的形式化语言(例如 PiSPEC 或 HLL)对系统的描述。

Formal Verification

形式化验证,即用数学方法自动证明系统满足某些精确要求。

GA

通用应用程序 (GA) 可以用作许多特定应用程序的基础。通用应用程序被足够详细地规范,以确保联锁软件能够自动生成、形式化验证和模拟特定应用程序。

GDS

通用设计规范(GDS)。 设计原则在通用设计规范中形式化。 它规定了如何设计生成的系统。

GNSS

全球导航卫星系统(Global Navigation Satellite System)是基于卫星的全球导航系统,可以依靠美国的GPS(全球定位系统)或俄罗斯的GLONASS(全球导航卫星系统)或欧洲正在开发的伽利略系统运行。

GSS

通用安全规范(GSS)。 安全要求在通用安全规范中形式化, 它设置了每个生成系统进行形式化验证的规定要求。

GTS

通用测试规范(GTS)。 功能需求在通用测试规范 (GTS) 中形式化, 它为每个生成的系统指定了通过仿真的方式进行检查的各项要求。

HLL

HLL 是一种高表达性的形式化语言,非常适合作为认证翻译的目标语言,以实现规范、设计和编码的各个方面。

HSL

高速线(HSL)是指速度超过 200 公里/小时(125 英里/小时)的铁路线。

IRIS

国际铁路行业标准。

IXL

一种列车控制等级。联锁系统用来负责列车在车站内、通过复杂的路口和线路中的可靠和安全移动。 而这一联锁系统确保了,只有当线路可以使用,且沿线道岔全都被安全锁定的情况下,列车的移动才被允许。在所有情况下,联锁都会一次为一列火车分配一个轨道路段或一条路线,同时排除其他所有火车的进入。

LRT

轻轨交通(LRT)是城市轨道交通的一种形式,它使用的设备和基础设施通常比地铁系统所用的要小,现代轻轨车辆通常沿着系统运行。

Model-based development

基于模型的开发,这是一种专注于创建和利用领域模型的软件开发方法,领域模型是与特定问题相关的所有主题的概念模型。 因此,它强调并针对管理特定应用领域的知识及活动的抽象描述,而不是计算(例如算法)概念。

Model checking

模型检查,它是一种形式化验证有限状态并发系统的方法。 关于系统的规范被表述为时序逻辑公式,高效的符号算法被用来通过系统定义模型,并用来检查规范是否成立。

Model transformation

模型转换,它是以模型为输入,生成目标模型作为输出,同时保持信息一致性的程序。 使用模型转换的目的是节省工作量,并在条件允许时通过自动化模型的构建和修改而减少错误。

OTP

优化流量规划(OTP) 是一种交通管理系统,允许实时监控整个铁路系统中列车的位置。优化流量规划通过安全地减少列车之间的时间来优化系统或网络容量,从而降低运营成本。优化流量规划主要是为那些铁路系统基础设施被充分利用的市场而设计的。

PiSPEC

PiSPEC 是一种规范语言,专为联锁系统的规范而设计,它基于世界各地工程类课程中所教授的众所周知的概念之上。

Predicate logic

谓词逻辑,或一阶逻辑(first-order logic),使用量化变量并允许使用包含谓词和变量的语句。

Process calculus

过程演算,用于描述独立的智能体或进程集合之间的交互、通信和同步的工具。它们还提供代数定律,允许操作和分析过程描述,并允许对过程之间的等价性进行形式化推理。

Proof obligation

证明义务,这是一个逻辑公式,它与特定验证属性的正确性声明相关联。当且仅当该性质在所有解释中都成立时,该公式才有效。该验证属性的正确性被“委托”来证明这个公式的正确性。

Propositional logic

命题逻辑,是运算 AND(并取)、OR(析取)、NOT(否定)和 IMPLIES(蕴涵)的形式化逻辑。

PTC

积极列车控制:北美货运铁路实施的基于通信的列车自动控制系统。

RAMS

可靠性、可用性、可维护性和安全性(Reliability, Availability, Maintainability and Safety)

RBI

继电器联锁,是一种联锁系统,由复杂的电路组成,这些电路由继电器组成,并以继电器逻辑排列以确定每个信号设备的状态或位置。

Refinement

程序细化,是将抽象(高级)形式化规范可验证地转换为具体(低级)可执行程序。

SA

特定应用程序 (SA) 是基于通用应用程序 (GA) 和特定应用程序配置数据(例如轨道布局、轨旁设备属性等)生成的。

Safety property

安全性能,为了使系统被认为是安全的,系统必须满足的属性。

SAT

布尔可满足性问题(有时称为命题可满足性问题,缩写为 SATISFIABILITY 或 SAT)是确定是否存在满足给定布尔公式的解释的问题。 换句话说,它询问给定布尔公式的变量是否可以以公式计算结果为 TRUE 的方式一致地替换为值 TRUE 或 FALSE。 如果是这种情况,则该公式称为可满足的。SAT 技术可用于证明或反驳属性:如果不能满足对属性的否定,则该属性有效。 如果某种描述满足了对属性的否定,那么这种解释就是该属性的反例。

Shift2Rail

Shift2Rail 将成为欧洲第一个铁路联合技术计划,旨在通过加速将新技术和先进技术集成到创新铁路产品解决方案中,来寻求重点研究和创新 (R&I) 以及市场驱动的解决方案。 Shift2Rail 将提升欧洲铁路行业的竞争力,并将满足不断变化的欧盟运输需求。

Soundness

健全性,当且仅当系统中可以证明的每个公式对于系统的语义都是有效的时候,一个形式化系统才是健全的。

SSI

SSI 是二十世纪80 年代由英国铁路研究部、英国通用电气公司(GEC-General Signal) 和英国西屋信号有限公司(Westinghouse Signals Ltd)开发的,第一代基于处理器的联锁的品牌名称。

State space

状态空间,是由系统中状态变量值的所有可能组合表示的一组系统状态。

State space explosion

状态空间爆炸,指随着系统中状态变量数量的增加,系统状态空间的大小呈指数增长。

Theorem proving

定理证明,处理通过计算机程序证明数学定理的自动推理和数理逻辑的一个子领域。 对数学证明的自动化推理是计算机科学发展的主要推动力。

TMS

交通管理系统。

UNIFE

欧洲铁路行业协会。