基于SCADE的安全軟件開發方法研究

陳淑珍，陳榮武，李 耀

（西南交通大學 信息科學與技術學院，成都 610031）

基于SCADE的安全軟件開發方法研究

陳淑珍，陳榮武，李 耀

（西南交通大學 信息科學與技術學院，成都 610031）

針對傳統軟件開發方式已經不能滿足高安全性系統安全性、完整性的需求，本文提出了基于SCADE的安全軟件開發方法，分析SCADE開發的原理、流程及應用方式，并以城市軌道交通列車運行控制系統的區域控制器ZC為例，基于SCADE對ZC列車管理功能進行建模和驗證。通過實例分析，證明基于SCADE的軟件開發方法，可以有效保障高安全性系統的安全性和完整性，為其提供了一種新的開發方式。

SCADE；軟件安全；軟件建模；區域控制器

高安全性應用開發環境 ( SCADE，Safety Critical ApplicationDevelopment Environment)，用基于模型的方式為高安全性系統提供完整的嵌入式開發解決方案，具有開發質量好、效率高、成本低、風險小、驗證時間短等優點。

SCADE 開發方式解決了傳統方式很多不足[1]。SCADE開發十分方便，且效率高，投入低，能夠保證軟件的質量，從以“代碼”為核心轉變為以“模型”為核心。以“代碼”為核心的開發方式，開發人員專注于編碼，主要關心的是軟件功能的實現；而以“模型”為核心的開發方式擺脫了枯燥的編碼，開發人員的注意力轉移到了軟件功能的正確性上，體現了軟件設計的真正意義，是軟件開發方式的發展方向。SCADE具有嚴格的數學語義，需求表達明確、無二義，能夠確保軟件的安全性和可靠性。

區域控制器（ZC，Zone Controller）是基于通信的列車控制系統 CBTC 的地面核心控制設備，保證列車行車安全。ZC系統安全性要求高，結構復雜，系統軟件需要滿足 EN 50128SIL 4 級標準，開發要求極為苛刻，傳統方式開發難度大。本文以其列車管理功能為例分析了 SCADE 開發的原理及流程，證明SCADE開發模式完全能夠滿足 ZC 系統需求，而且具有效率高，成本低，結構清楚，軟件質量好，安全性和可靠性有保障等優點。

1 理論基礎

SCADE 開發基于同步假設，而且以 Lustre 為核心，這兩點也決定了 SCADE 開發的特點。

1.1 反應式系統

反應式系統是相對于轉換式系統而言的，其與環境保持不間斷交互，隨時接受來自環境的刺激，運算后做出響應，環境可能利用該響應繼續為系統提供新的輸入。這個過程可能不是順序的，其行為具有并發性、不終止性等特點，并不是最終產生一個輸出。

1.2 同步假設

同步理論模型是基于周期執行模型的擴展，在每個周期內，模型以傳感器采樣或通信等方式獲得輸入，隨即進行處理，最后將處理結果輸出給目標模塊或系統。在一個計算周期內，模型和環境之間沒有任何交互，程序的行為是確定的。

同步假設是假設反應式系統響應速度足夠快，系統接收環境輸入后立即響應，然后產生輸出，并等待下一個輸入，在此期間，系統內部狀態保持不變，如圖1所示。

圖1 同步假設模型

在實際中，由于技術或成本的限制，一般是通過控制系統獲得任意兩次輸入的時間間隔大于系統的響應時間的方式來實現同步假設的。即：

Ti—系統第 i次輸入的時間

Ti+1—系統第 i+1 次輸入的時間T?—系統響應的時間

1.3 Lustre

Lustre 是基于數據流的同步編程語言，適用于反應系統，通過劃分物理時間的方式建立同步模型。Lustre 每一個變量都代表一個數據流，流是一個給定數據類型的值的無限序列，具有數值和時鐘兩個特性，如等式 x=f，表示 An, xn=fn，n 為周期。Lustre提供的時間運算符，對數據流進行采樣，也可以獲取之前周期的流值，對控制系統的建模提供了方便。

如一個帶有兩個輸入 a,b 和重啟按鈕 reset的計數器，有如下需求：

（1）初始顯示 0；

（2）當按下重啟按鈕時，計數器輸出 0；

（3）兩個輸入和大于 50 時，計數器輸出不變；

（4）否則計數器每個周期的值加 1。該計數器的 Lustre 表達如圖 2 所示：初始化運算符“→”用于初始每個流第一個周期的值，用 n表示周期，則 An，

圖2 計數器Lustre表達1

“Pre”運算符表示取上一周期的值，用 n 表示周期，則：

Lustre 是一種聲明式語言，關注計算機應該做什么，不是命令式語言所關注的計算機應該如何做。Lustre 語言的語句具有順序無關性；例如：此計數器中語句：c=0 → (a+b)在圖 2 和圖 3 中的陳述順序是不一樣的，但是它們所表示的節點在本質上一樣。

圖3 計數器Lustre表達2

理解理論基礎對 SCADE 模型提取、理解等十分必要，特別是復雜系統。

2 模型建立

SCADE 模型是需求的一種明確、無歧義的表達，提供文本和圖形兩種建模方式，文本方式使用 Lustre語言，圖形方式包括安全狀態機和數據流圖。這些建模機制都建立在嚴格的數學模型之上，具有嚴格的數學語義，保證了模型的完整性、精確性、一致性和無二義性。在實際使用中，圖形方式使用相對較多，而且圖形化建模時，可以觀察到節點的 Lustre表達方式，還可以自動轉化為文本節點。

2.1 安全狀態機

安全狀態機常用于描述控制系統的狀態及邏 輯 功 能 ， 是 控 制 流 和 判 定 邏 輯 的 直 觀 模 型 ，常用于離散系統建模，具有順序控制，并發控制，層次控制的結構特點[5]。安全狀態機是有限狀態機的拓展，其中的狀態也是有限的。

安全狀態機用“狀態”描述系統的一種模式，用“遷移”描述模式之間的轉移，用“信號”反應狀態機和環境之間的交互。遷移分為強連接遷移、弱連接遷移及同步連接遷移，每個遷移都具有各自的優先級，遷移由遷移標識控制。遷移觸發后，在進入狀態，處于狀態和離開狀態時都可能完成相關操作。根據SCADE的這些特點，安全狀態機能夠描述復雜系統的邏輯結構，確保模型的確定性。對控制結構豐富而數據處理較少的模型，十分適合使用安全狀態機。

ZC是典型的高安全性系統，其安全性、可靠性關系到 CBTC 系統的正常運行，SCADE 開發完全滿足ZC系統的特點和需求。列車管理是 ZC系統的重要功能之一，根據列車的不同行為，可以將列車狀態簡單概括為以下幾種狀態：初始狀態，正常運行狀態，注銷狀態。ZC 的 SCADE 列車管理功能安全狀態機如圖4所示。

圖4 SCADE ZC列車管理功能安全狀態機圖

SCADE 安全狀態機支持狀態機嵌套，但每個狀態機都必須有明確的初始狀態，圖4中黑粗邊框的狀態即為初始狀態。圖4中各狀態及變遷含義如表1所示。列車首先處于初始狀態 S_Init，當 T_I2N 轉移條件滿足時，轉移到列車正常運行狀態；當 T_N2L條件滿足時，則由正常運行狀態轉移到列車注銷狀態；當 Y_L2I條件繼續滿足時，則由列車注銷狀態轉移到列車初始狀態。

2.2 數據流圖

數據流圖善于描述數據的處理過程，反應時序及因果關系，常常用于連續系統的建模。數據流圖通過用戶定義的輸入變量接收外界信號，經過模型處理后，再以用戶定義的輸出變量為接口輸出給目標模塊或系統。節點是數據流圖的最基本的功能單元，類似于C語言的函數。數據流圖提供算術運算、邏輯運算、比較運算，時間運算等運算符，SCADE利用這些運算符及自定義的運算符，以圖形化的方式構建新的更復雜的節點，完成更復雜的功能。對復雜控制結構較少而數據處理較多的模型，適合使用數據流圖。

表1 列車管理功能狀態機圖的狀態含義

ZC 折反請求的 SCADE 數據流圖如圖 5所示，當 ZC 獲取列車狀態運算符 GetTrainState 解析到列車信息 I_Train_Info 為折返列車 REVERSE_TRAIN并且獲取進路類型運算符 GetRouteType 解析到進路信息 I_RoutInfo 為折返進路 REVERSE_ROUTE 時，觸發折返轉移 T_M2R，列車將進入折返狀態。

圖5 折返條件數據流圖

這兩種建模方式不是獨立的，可相互結合使用。

3 模型驗證

系統可靠性、安全性依賴于系統功能的正確性。在軟件開發流程中，SCADE的驗證處于代碼之前，表達需求時就對功能進行了驗證。開發人員的注意力轉移到了需求的合理性、模型的正確性，提高了軟件的質量和開發效率。

對于已經建立的模型，SCADE提供兩種方式進行驗證：模擬仿真和形式化驗證。在系統開發早期使用模擬仿真，而在設計的最后階段使用形式化驗證。

3.1 模擬仿真

SCADE仿真對象可以是整個系統，也可以是一個模塊或子系統。對仿真過程中模型的輸入、輸出以及內部變量，SCADE仿真器提供了文本和圖形兩種觀察方式。文本方式展示輸入、輸出或所觀察變量在當前周期的值，圖形方式展示了所有周期的數據，直觀的反應了數據的變化趨勢。

SCADE 的仿真并不是直接對圖形模型進行仿真，而是先生成C代碼，再通過執行C代碼達到仿真的目的，即是對代碼生成器生成的目標代碼的執行。這樣模擬仿真的結果和將來目標代碼的執行結果完全相同。

SCADE仿真是仿真器在當前模型下對外部輸入的響應，由于模型已經建立，所以可以通過保存仿真過程中所有周期輸入數據的方式保存仿真場景。仿真器載入仿真場景后，模型和輸入數據都具備，所以可以繼續仿真。

SCADE仿真器支持單步、多步、單步后退及多步后退等仿真方式，還支持批處理模式仿真，在多測試用例中十分方便。

3.2 模型測試覆蓋率MTC

仿真是通過觀察模型對指定輸入的響應情況來分析系統功能的正確性，所以測試案例的數量及質量關系到測試的完備程度及深度。SCADE提供DC和 MC/DC 兩種覆蓋率準則，定量分析仿真測試的完備程度及深度，包括覆蓋率提取，覆蓋率分析，覆蓋率處理，生成覆蓋率報告4個步驟。如果覆蓋率未達 100%，SCADE 將給出未覆蓋的路徑。

在開發的早期階段，覆蓋率分析可以幫助開發人員發現眾多問題，如模型設計錯誤，測試案例不足等。模擬仿真是對模型的驗證，MTC是對仿真的驗證，即是驗證的驗證。

3.3 形式化驗證

SCADE 提供形式化驗證的方式保證安全需求。

傳統的形式化驗證方法主要缺點是對原始設計進行模型提取時，一般需要使用某種語言構造數學模型，再利用相關工具進行數學推理，這對驗證者的數學技能和經驗要求較高。SCADE形式驗證避免了這些不足，其建模語言即是驗證語言，一種語言完成建模和驗證兩個功能。

SCADE 形式化驗證與仿真測試，如表 2所示。

3.3.1 提取安全屬性

表2 形式驗證與模擬仿真的區別

安全屬性為保證系統不會發生危險的屬性，如“CBTC 系統中，列車不能越過 MA 停車”。安全屬性一般來自于設計規范及需求等。

3.3.2 方式的轉換

建立安全特征觀察器 Observer，即在形式化驗證器中用數據流圖的方式將安全需求轉換為圖形表達。Observer本質上也是 SCADE 的節點 ,但是多了一些特定的驗證運算符，而且輸出始終為一 Boolean變量且應當為 true。

這兩步都是人工完成，對設計者的專業知識及技能有一定的要求。驗證器不能檢測 Observer模型的正確性，如果提取了錯誤的安全屬性，或 Observer建立錯誤，驗證器將以錯誤的安全屬性驗證模型，這也是 SCADE 的不足之一。

3.3.3 驗證安全屬性

安全屬性的驗證是證明該屬性在目標模型所有周期和所有場景下都是正確的。SCADE將待驗證模型和 Observer模型結合，利用待驗證模型的輸入、輸出信號自動驗證模型是否滿足安全需求。如果不能，Observer輸出 false，同時 SCADE 給出一個可導入仿真器分析的反例；如果滿足，Observer輸出true, 同時 SCADE 給出安全證明。

ZC列車管理功能有如下安全要求：每一時刻，列車最多只能向一個狀態轉移。對SCADE功能模型，該安全需求的含義是：同一時刻最多只有一個轉移條件為真。SCADE 提供了 Sharp 運算符 #，當其輸入條件最多只有一個為真時，Sharp 輸出 true 信號，其 Observer模型如圖 7，圖中變量在表 1 中有注明。模型的輸入為列車狀態轉移的所有條件。當 T_I2N，T_N2L 和 Y_L2I共 3 個狀態轉移條件最多只有一個為真時輸出結果 Result才會為真。

圖6 形式驗證過程

圖7 安全特征觀察器模型

SCADE 為驗證功能提供了大量的預定義運算符，降低了驗證的難度和復雜度。通過不到一秒的驗證，SCADE 證明模型滿足此安全需求。

4 目標代碼

SCADE 開發的最終目標就是生成可信代碼。SCADE 的代碼生成器 KCG 通過了 DO-178B A 級、IEC 61508 SIL3、EN 50128 3/4、IEC 60880 認證，生成的代碼滿足安全特性，如有界的堆棧。KCG將SCADE 的圖形模型作為輸入，根據用戶設定的參數，輸出目標代碼和可跟蹤文件，如圖8所示。

圖8 KCG模型

KCG 前端模塊將模型文件轉換為 SCADE 程序，復制注釋信息，刪除圖形相關信息，并進行語法語義檢查；中間模塊是編譯核心和優化器；后端模塊生成目標代碼和可追蹤文件[5]。

對于已經完成設計的模型，只需點擊“生成”按鈕，SCADE 自動將圖形模型轉換為 ANSIC 或ADA代碼和可追蹤文件，包括模型中的注釋信息。

4.1 圖形模型轉換為Lustre語言

將節點、狀態圖等圖形元素轉換成 Lustre 語言描述的模型，并將多個文件模型整合到一個文件中。

4.2 Lustre語言轉換為目標語言

目標代碼是完全面向工程的代碼，可以不做任何修改直接將代碼移植到目標模塊中，但 SCADE 生成的代碼可讀性不如人工代碼。

SCADE生成的代碼執行效果與之前仿真效果完全一致，在保證功能正確后，不需要對目標代碼進行任何驗證，從而節省了大量測試時間，而且代碼具有可追蹤、可移植、模塊化、代碼優化、有限運行時段等特性，同時KCG支持批量生成代碼。

5 結束語

SCADE開發方式覆蓋了嵌入式開發從需求到代碼的所有流程，包括需求管理、需求建模、模型檢查、模擬仿真、測試覆蓋率分析、形式驗證、文檔生成、代碼生成等。其操作方便，使用形式化的方法保證設計的無二義性、正確性，自動生成高質量代碼，能夠在軟件開發的早期階段發現錯誤，節約軟件開發成本，提高軟件開發的效率和質量，縮短軟件面市時間，提高軟件開發的自動化程度，并為軟件認證提供支持，非常適合高安全性系統的開發。

但 SCADE 也有不足之處需要改進，如對于復雜的邏輯功能，需要導入用戶自定義的節點，但KCG生成代碼時對此部分沒有驗證。

[1] 張 路 .基于 SCADE 的 CBTC 區域控制器軟件開發 [D].北京：北京交通大學，2010.

[2] 高 霖 .CBTC 區域控制系統中列車管理的建模與分析 [D].北京：北京交通大學，2007.

[3] 胡鋼偉 ,李振水 ,高亞奎 . SCADE 軟件開發方法研究 [J].系統仿真學報，2008（S2)：286-288.

[4] 林 楓 .基于 SCADE 的形式化驗證技術研究 [J].測控技 術，2011，30（12）：71-74.

責任編輯 徐侃春

Method of SCADE-based safety software development

CHEN Shuzhen, CHEN Rongwu, LI Yao
( School of Information Science and Technology, Southwest Jiaotong University, Chengdu 610031, China )

The traditional methods of software development couldn’t meet the requirements of high security and integrity of safety critical system. The article proposed the method of SCADE-based safety software development, analyzed the principle, process and application methods of SCADE. The ZC of Urban Transit was taken as an example, through modeling and verifying the train management functions of ZC, it was proved that this method provided a new method which could eff i ciently ensure the high security and integrity of safety critical system.

SCADE; software safety; software modeling; Zone Controller(ZC)

U284.482∶TP39

：A

1005-8451（2015）03-0014-05

2014-08-02

陳淑珍，在讀碩士研究生；陳榮武，高級工程師。