在軌道交通領(lǐng)域，實(shí)現(xiàn)信號(hào)控制的計(jì)算機(jī)為故障安全型計(jì)算機(jī)，為了兼顧安全性和可用性的要求，采用三取二和二乘二取二的安全架構(gòu)居多。這種架構(gòu)采用兩個(gè)以上的處理單元構(gòu)成，需要兩個(gè)處理單元的計(jì)算結(jié)果一致或三個(gè)中至少有兩個(gè)計(jì)算結(jié)果一致，再對(duì)外輸出。目前大多數(shù)信號(hào)系統(tǒng)的安全平臺(tái)都是這兩種架構(gòu)之一，那么，是否有單一計(jì)算通道能夠?qū)崿F(xiàn)故障安全呢，答案也是有的，本文來(lái)介紹下一種典型的單處理器安全計(jì)算機(jī)——SACEM。

SACEM，是法文的縮寫，全稱為System d' Aide a` la Conduite a` l' Exploitation et a` la Maintenance（駕駛輔助、操作及維護(hù)系統(tǒng)）。由巴黎公共交通管理局RATP和法國(guó)鐵路局SNCF主導(dǎo)，GEC ALSTHOM TRANSPORT組織包括MATRA TRANSPORT和CSEE TRANSPORT開發(fā)。SACEM最早在上個(gè)世紀(jì)1982年開始研發(fā)，1988年研發(fā)完成并應(yīng)用于巴黎地鐵RER A線路。

SACEM系統(tǒng)實(shí)現(xiàn)列車的安全防護(hù)，包括列車之間的安全間距防護(hù)，列車的超速防護(hù)，進(jìn)入道岔區(qū)間防護(hù)和軌旁信號(hào)向車載信號(hào)的傳遞。SACEM系統(tǒng)也具備ATO自動(dòng)駕駛功能，能夠?qū)崿F(xiàn)自動(dòng)的加速、減速、停站等功能。SACEM系統(tǒng)由軌旁安全計(jì)算機(jī)和車載安全計(jì)算機(jī)構(gòu)成，三十年前還沒(méi)有WLAN或LTE車地?zé)o線系統(tǒng)，列車車載設(shè)備與軌旁設(shè)備通過(guò)軌道電路和環(huán)線單向傳輸前車的位置、列車停車點(diǎn)等信息。

每一段區(qū)間設(shè)置軌旁計(jì)算機(jī)，其功能是收集來(lái)自列車的信息探測(cè)、運(yùn)行路線和信號(hào)的狀態(tài)，并收集來(lái)自列車的信息。從這些可變數(shù)據(jù)和該區(qū)間的固定數(shù)據(jù)中產(chǎn)生軌道到列車的傳輸信息。

每列車的車載計(jì)算機(jī)接收到的信息是軌道與列車之間的傳輸，列車的各種狀態(tài)(運(yùn)行方向、列車長(zhǎng)度等），以及由固定信標(biāo)讀取的基準(zhǔn)點(diǎn)和測(cè)速編碼器提供的累積距離。

SACEM系統(tǒng)安全性滿足最高安全完整性等級(jí)SIL4要求，即由系統(tǒng)引起的災(zāi)難性失效發(fā)生頻率低于每列車10E-9/h。同時(shí)，也要求具備極高的可用性，由系統(tǒng)引起的誤停車發(fā)生頻率低于每列車2*10E-3/h。

對(duì)于列車控制的信號(hào)系統(tǒng)基本原理與業(yè)內(nèi)常見的信號(hào)系統(tǒng)沒(méi)有太大差異，SACEM系統(tǒng)的特點(diǎn)在于它實(shí)現(xiàn)信號(hào)控制的安全計(jì)算機(jī)硬件和軟件技術(shù)，采用了編碼計(jì)算和形式化方法這兩種安全技術(shù)。

編碼計(jì)算技術(shù)

編碼計(jì)算技術(shù)通過(guò)分析計(jì)算機(jī)運(yùn)算時(shí)存在的三種錯(cuò)誤類型：

operation error（操作數(shù)錯(cuò)誤）：計(jì)算機(jī)使用預(yù)期操作符處理操作數(shù)得到了錯(cuò)誤的結(jié)果。這種類型的錯(cuò)誤，非常類似于傳輸錯(cuò)誤，但不會(huì)給代碼設(shè)計(jì)帶來(lái)新的約束。

operator error（操作符錯(cuò)誤）：計(jì)算機(jī)使用好的操作數(shù)，但有一個(gè)非預(yù)期的運(yùn)算符。例如，如果一個(gè)加法運(yùn)算符被替換成乘法運(yùn)算符，結(jié)果是假的，即使乘法計(jì)算的結(jié)果是正確的。對(duì)這種類型的錯(cuò)誤的檢測(cè)，不是數(shù)據(jù)傳輸通道存在的錯(cuò)誤，需要對(duì)運(yùn)算符增加編碼。

operand error（操作錯(cuò)誤）：一種情況是地址錯(cuò)誤，相當(dāng)于用一個(gè)變量替換了另一個(gè)變量。這種類型的錯(cuò)誤發(fā)生在傳輸系統(tǒng)中，在不同的通道之間發(fā)生了串?dāng)_的。類似于傳輸過(guò)程中收到了發(fā)送到另一個(gè)接收者的數(shù)據(jù)。另一種情況是存儲(chǔ)錯(cuò)誤，存儲(chǔ)的數(shù)據(jù)變化或者沒(méi)有被更新，是過(guò)時(shí)的數(shù)據(jù)。

因此，為了防護(hù)以上三類計(jì)算機(jī)錯(cuò)誤，采用了以下三種編碼技術(shù)：

a) 算術(shù)編碼arithmetical code：用來(lái)檢測(cè)信息存儲(chǔ)和傳輸?shù)腻e(cuò)誤。信息存儲(chǔ)和傳輸?shù)腻e(cuò)誤，以及 操作錯(cuò)誤（不正確的指令 執(zhí)行）。

b) 簽名技術(shù)signature：用于檢測(cè)運(yùn)算符和操作數(shù)的錯(cuò)誤，以及操作結(jié)果的錯(cuò)誤，程序順序的錯(cuò)誤。

c) 動(dòng)態(tài)化技術(shù)dynamisation：用來(lái)檢測(cè)信息的實(shí)時(shí)性，通過(guò)給每個(gè)計(jì)算周期分配一個(gè)日期，檢測(cè)信息刷新的錯(cuò)誤。

上面是算術(shù)編碼的一個(gè)實(shí)例，選擇A=9，k=4，我們有2k=16和-2k[A]=2。數(shù)據(jù)X=5被編碼為81，數(shù)據(jù)Y=7被編碼為117，X和Y的相加得到198。對(duì)Z的解碼（提取高權(quán)重的比特）得到Z=12，編碼的正確性可通過(guò)198[A]=0得到驗(yàn)證。

SACEM車載和軌旁安全計(jì)算機(jī)架構(gòu)

編碼計(jì)算機(jī)架構(gòu)

上圖中，SACEM系統(tǒng)的車載計(jì)算機(jī)和軌旁計(jì)算機(jī)中的運(yùn)算單元均采用編碼計(jì)算技術(shù)，通過(guò)以上三種編碼技術(shù)來(lái)檢測(cè)硬件出現(xiàn)的任何隨機(jī)故障。編碼計(jì)算機(jī)在每個(gè)運(yùn)算周期結(jié)束時(shí)，會(huì)計(jì)算出附加的編碼變量值，這個(gè)變量是由所有輸出值的組合計(jì)算出來(lái)的，再根據(jù)算術(shù)代碼解碼。對(duì)于該變量的時(shí)間值，在處理器外，與算術(shù)代碼或時(shí)間值有關(guān)的錯(cuò)誤都會(huì)被轉(zhuǎn)移到周期更新的簽名中，通過(guò)故障安全比較器與參考簽名進(jìn)行比較。比較一致后認(rèn)為本運(yùn)算周期輸出的結(jié)果是可信的。一致性輸出結(jié)果用于控制了一個(gè)固有式故障安全的電源，當(dāng)檢測(cè)結(jié)果不一致時(shí)，會(huì)使電源失電從而輸出最終的緊急制動(dòng)。

對(duì)于軟件編譯工具產(chǎn)生的錯(cuò)誤，由于編碼計(jì)算的原理是每周期獨(dú)立地計(jì)算簽名，對(duì)于編譯錯(cuò)誤同樣屬于操作數(shù)錯(cuò)誤，也能夠檢測(cè)出來(lái)。

編碼技術(shù)的優(yōu)勢(shì)在于它基于數(shù)學(xué)原理設(shè)計(jì)了編碼算法，因此無(wú)需依賴于專用的硬件，同樣能夠?qū)崿F(xiàn)對(duì)計(jì)算機(jī)運(yùn)算時(shí)出現(xiàn)的各類故障類型進(jìn)行檢測(cè)。

形式化技術(shù)

除了硬件隨機(jī)性故障和軟件操作運(yùn)算中出現(xiàn)的故障，導(dǎo)致安全計(jì)算機(jī)出錯(cuò)的因素還有來(lái)自需求和設(shè)計(jì)實(shí)現(xiàn)錯(cuò)誤產(chǎn)生的系統(tǒng)性故障，為解決不規(guī)范的軟件規(guī)范問(wèn)題，需求規(guī)范的含糊不清、不清晰、不連貫、不完整，對(duì)需求的驗(yàn)證確認(rèn)問(wèn)題，如何確定功能測(cè)試的充分性，SACEM系統(tǒng)的軟件設(shè)計(jì)采用了形式化語(yǔ)言的設(shè)計(jì)方法——B方法。

B方法并不僅僅是一種編程語(yǔ)言，它是設(shè)計(jì)方法，編程語(yǔ)言、開發(fā)及驗(yàn)證工具鏈的組合。它的目標(biāo)是為了構(gòu)建完全滿足其定義需求的軟件，B方法定義了用于軟件需求的抽象運(yùn)算符和類似于ADA或C語(yǔ)言的具體編程指令，采用了面向模型的方法，即軟件=數(shù)據(jù)+屬性+操作；能夠?qū)⑿枨竽Ｐ娃D(zhuǎn)換成具體模塊，并最終轉(zhuǎn)化為代碼。通過(guò)嚴(yán)格的數(shù)學(xué)結(jié)構(gòu)來(lái)檢查軟件需求規(guī)范的正確性、完整性。

形式化方法的驗(yàn)證過(guò)程是通過(guò)將非規(guī)范化的軟件轉(zhuǎn)換為形式化需求，逐級(jí)分解細(xì)化，每一級(jí)都采用數(shù)學(xué)模型進(jìn)行一致性驗(yàn)證，因此它不再需要軟件的單元測(cè)試和集成測(cè)試，只進(jìn)行對(duì)軟件需求的確認(rèn)測(cè)試。

形式化方法的逐級(jí)證明

形式化方法的驗(yàn)證確認(rèn)

SACEM系統(tǒng)在國(guó)外的不少地鐵線路中有應(yīng)用，但在國(guó)內(nèi)的軌道交通領(lǐng)域，無(wú)論是國(guó)鐵還是地鐵，都不是主流技術(shù)，沒(méi)有得到引進(jìn)、吸收轉(zhuǎn)化和推廣，國(guó)內(nèi)的應(yīng)用和熟悉這類技術(shù)的人不是很多。但其作為安全計(jì)算機(jī)的一個(gè)技術(shù)流派，至今也有三十多年的歷史了，有著它自身的特點(diǎn)。它的設(shè)計(jì)思想能夠體現(xiàn)正向設(shè)計(jì)，如何解決konw-how的問(wèn)題，簡(jiǎn)單來(lái)說(shuō)，也是第一性原理的體現(xiàn)，實(shí)現(xiàn)安全設(shè)計(jì)的技術(shù)手段是多樣性的，可以是多重處理器的冗余比較，可以是單處理器的編碼計(jì)算，也可以是其它的技術(shù)方法，但前提都從解決問(wèn)題的本質(zhì)出發(fā)，不可機(jī)械套用而不得其機(jī)理。

審核編輯：郭婷