专业知识

Balise

CBI

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

CBTC

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

CENELEC

欧洲电工标准化委员会。

Completeness

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

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

欧洲铁路行业协会。