典型单处理器安全计算机SACEM的介绍

在轨道交通领域，实现信号控制的计算机为故障安全型计算机，为了兼顾安全性和可用性的要求，采用三取二和二乘二取二的安全架构居多。这种架构采用两个以上的处理单元构成，需要两个处理单元的计算结果一致或三个中至少有两个计算结果一致，再对外输出。目前大多数信号系统的安全平台都是这两种架构之一，那么，是否有单一计算通道能够实现故障安全呢，答案也是有的，本文来介绍下一种典型的单处理器安全计算机——SACEM。

SACEM，是法文的缩写，全称为System d' Aide a` la Conduite a` l' Exploitation et a` la Maintenance（驾驶辅助、操作及维护系统）。由巴黎公共交通管理局RATP和法国铁路局SNCF主导，GEC ALSTHOM TRANSPORT组织包括MATRA TRANSPORT和CSEE TRANSPORT开发。SACEM最早在上个世纪1982年开始研发，1988年研发完成并应用于巴黎地铁RER A线路。

SACEM系统实现列车的安全防护，包括列车之间的安全间距防护，列车的超速防护，进入道岔区间防护和轨旁信号向车载信号的传递。SACEM系统也具备ATO自动驾驶功能，能够实现自动的加速、减速、停站等功能。SACEM系统由轨旁安全计算机和车载安全计算机构成，三十年前还没有WLAN或LTE车地无线系统，列车车载设备与轨旁设备通过轨道电路和环线单向传输前车的位置、列车停车点等信息。

每一段区间设置轨旁计算机，其功能是收集来自列车的信息探测、运行路线和信号的状态，并收集来自列车的信息。从这些可变数据和该区间的固定数据中产生轨道到列车的传输信息。

每列车的车载计算机接收到的信息是轨道与列车之间的传输，列车的各种状态(运行方向、列车长度等），以及由固定信标读取的基准点和测速编码器提供的累积距离。

SACEM系统安全性满足最高安全完整性等级SIL4要求，即由系统引起的灾难性失效发生频率低于每列车10E-9/h。同时，也要求具备极高的可用性，由系统引起的误停车发生频率低于每列车2*10E-3/h。

对于列车控制的信号系统基本原理与业内常见的信号系统没有太大差异，SACEM系统的特点在于它实现信号控制的安全计算机硬件和软件技术，采用了编码计算和形式化方法这两种安全技术。

编码计算技术

编码计算技术通过分析计算机运算时存在的三种错误类型：

operation error（操作数错误）：计算机使用预期操作符处理操作数得到了错误的结果。这种类型的错误，非常类似于传输错误，但不会给代码设计带来新的约束。

operator error（操作符错误）：计算机使用好的操作数，但有一个非预期的运算符。例如，如果一个加法运算符被替换成乘法运算符，结果是假的，即使乘法计算的结果是正确的。对这种类型的错误的检测，不是数据传输通道存在的错误，需要对运算符增加编码。

operand error（操作错误）：一种情况是地址错误，相当于用一个变量替换了另一个变量。这种类型的错误发生在传输系统中，在不同的通道之间发生了串扰的。类似于传输过程中收到了发送到另一个接收者的数据。另一种情况是存储错误，存储的数据变化或者没有被更新，是过时的数据。

因此，为了防护以上三类计算机错误，采用了以下三种编码技术：

a) 算术编码arithmetical code：用来检测信息存储和传输的错误。信息存储和传输的错误，以及 操作错误（不正确的指令 执行）。

b) 签名技术signature：用于检测运算符和操作数的错误，以及操作结果的错误，程序顺序的错误。

c) 动态化技术dynamisation：用来检测信息的实时性，通过给每个计算周期分配一个日期，检测信息刷新的错误。

上面是算术编码的一个实例，选择A=9，k=4，我们有2k=16和-2k[A]=2。数据X=5被编码为81，数据Y=7被编码为117，X和Y的相加得到198。对Z的解码（提取高权重的比特）得到Z=12，编码的正确性可通过198[A]=0得到验证。

SACEM车载和轨旁安全计算机架构

编码计算机架构

上图中，SACEM系统的车载计算机和轨旁计算机中的运算单元均采用编码计算技术，通过以上三种编码技术来检测硬件出现的任何随机故障。编码计算机在每个运算周期结束时，会计算出附加的编码变量值，这个变量是由所有输出值的组合计算出来的，再根据算术代码解码。对于该变量的时间值，在处理器外，与算术代码或时间值有关的错误都会被转移到周期更新的签名中，通过故障安全比较器与参考签名进行比较。比较一致后认为本运算周期输出的结果是可信的。一致性输出结果用于控制了一个固有式故障安全的电源，当检测结果不一致时，会使电源失电从而输出最终的紧急制动。

对于软件编译工具产生的错误，由于编码计算的原理是每周期独立地计算签名，对于编译错误同样属于操作数错误，也能够检测出来。

编码技术的优势在于它基于数学原理设计了编码算法，因此无需依赖于专用的硬件，同样能够实现对计算机运算时出现的各类故障类型进行检测。

形式化技术

除了硬件随机性故障和软件操作运算中出现的故障，导致安全计算机出错的因素还有来自需求和设计实现错误产生的系统性故障，为解决不规范的软件规范问题，需求规范的含糊不清、不清晰、不连贯、不完整，对需求的验证确认问题，如何确定功能测试的充分性，SACEM系统的软件设计采用了形式化语言的设计方法——B方法。

B方法并不仅仅是一种编程语言，它是设计方法，编程语言、开发及验证工具链的组合。它的目标是为了构建完全满足其定义需求的软件，B方法定义了用于软件需求的抽象运算符和类似于ADA或C语言的具体编程指令，采用了面向模型的方法，即软件=数据+属性+操作；能够将需求模型转换成具体模块，并最终转化为代码。通过严格的数学结构来检查软件需求规范的正确性、完整性。

形式化方法的验证过程是通过将非规范化的软件转换为形式化需求，逐级分解细化，每一级都采用数学模型进行一致性验证，因此它不再需要软件的单元测试和集成测试，只进行对软件需求的确认测试。

形式化方法的逐级证明

形式化方法的验证确认

SACEM系统在国外的不少地铁线路中有应用，但在国内的轨道交通领域，无论是国铁还是地铁，都不是主流技术，没有得到引进、吸收转化和推广，国内的应用和熟悉这类技术的人不是很多。但其作为安全计算机的一个技术流派，至今也有三十多年的历史了，有着它自身的特点。它的设计思想能够体现正向设计，如何解决konw-how的问题，简单来说，也是第一性原理的体现，实现安全设计的技术手段是多样性的，可以是多重处理器的冗余比较，可以是单处理器的编码计算，也可以是其它的技术方法，但前提都从解决问题的本质出发，不可机械套用而不得其机理。

审核编辑：郭婷