在軌道交通領域，實現信號控制的計算機為故障安全型計算機，為了兼顧安全性和可用性的要求，采用三取二和二乘二取二的安全架構居多。這種架構采用兩個以上的處理單元構成，需要兩個處理單元的計算結果一致或三個中至少有兩個計算結果一致，再對外輸出。目前大多數信號系統的安全平臺都是這兩種架構之一，那么，是否有單一計算通道能夠實現故障安全呢，答案也是有的，本文來介紹下一種典型的單處理器安全計算機——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的問題，簡單來說，也是第一性原理的體現，實現安全設計的技術手段是多樣性的，可以是多重處理器的冗余比較，可以是單處理器的編碼計算，也可以是其它的技術方法，但前提都從解決問題的本質出發，不可機械套用而不得其機理。

審核編輯：郭婷