陳淑珍，陳榮武，李 耀

（西南交通大學(xué) 信息科學(xué)與技術(shù)學(xué)院，成都 610031）

基于SCADE的安全軟件開發(fā)方法研究

陳淑珍，陳榮武，李 耀

（西南交通大學(xué) 信息科學(xué)與技術(shù)學(xué)院，成都 610031）

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

SCADE；軟件安全；軟件建模；區(qū)域控制器

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

SCADE 開發(fā)方式解決了傳統(tǒng)方式很多不足[1]。SCADE開發(fā)十分方便，且效率高，投入低，能夠保證軟件的質(zhì)量，從以“代碼”為核心轉(zhuǎn)變?yōu)橐浴澳Ｐ汀睘楹诵摹Ｒ浴按a”為核心的開發(fā)方式，開發(fā)人員專注于編碼，主要關(guān)心的是軟件功能的實現(xiàn)；而以“模型”為核心的開發(fā)方式擺脫了枯燥的編碼，開發(fā)人員的注意力轉(zhuǎn)移到了軟件功能的正確性上，體現(xiàn)了軟件設(shè)計的真正意義，是軟件開發(fā)方式的發(fā)展方向。SCADE具有嚴(yán)格的數(shù)學(xué)語義，需求表達明確、無二義，能夠確保軟件的安全性和可靠性。

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

1 理論基礎(chǔ)

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

1.1 反應(yīng)式系統(tǒng)

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

1.2 同步假設(shè)

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

同步假設(shè)是假設(shè)反應(yīng)式系統(tǒng)響應(yīng)速度足夠快，系統(tǒng)接收環(huán)境輸入后立即響應(yīng)，然后產(chǎn)生輸出，并等待下一個輸入，在此期間，系統(tǒng)內(nèi)部狀態(tài)保持不變，如圖1所示。

圖1 同步假設(shè)模型

在實際中，由于技術(shù)或成本的限制，一般是通過控制系統(tǒng)獲得任意兩次輸入的時間間隔大于系統(tǒng)的響應(yīng)時間的方式來實現(xiàn)同步假設(shè)的。即：

Ti—系統(tǒng)第 i次輸入的時間

Ti+1—系統(tǒng)第 i+1 次輸入的時間T?—系統(tǒng)響應(yīng)的時間

1.3 Lustre

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

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

（1）初始顯示 0；

（2）當(dāng)按下重啟按鈕時，計數(shù)器輸出 0；

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

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

圖2 計數(shù)器Lustre表達1

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

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

圖3 計數(shù)器Lustre表達2

理解理論基礎(chǔ)對 SCADE 模型提取、理解等十分必要，特別是復(fù)雜系統(tǒng)。

2 模型建立

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

2.1 安全狀態(tài)機

安全狀態(tài)機常用于描述控制系統(tǒng)的狀態(tài)及邏 輯 功 能 ， 是 控 制 流 和 判 定 邏 輯 的 直 觀 模 型 ，常用于離散系統(tǒng)建模，具有順序控制，并發(fā)控制，層次控制的結(jié)構(gòu)特點[5]。安全狀態(tài)機是有限狀態(tài)機的拓展，其中的狀態(tài)也是有限的。

安全狀態(tài)機用“狀態(tài)”描述系統(tǒng)的一種模式，用“遷移”描述模式之間的轉(zhuǎn)移，用“信號”反應(yīng)狀態(tài)機和環(huán)境之間的交互。遷移分為強連接遷移、弱連接遷移及同步連接遷移，每個遷移都具有各自的優(yōu)先級，遷移由遷移標(biāo)識控制。遷移觸發(fā)后，在進入狀態(tài)，處于狀態(tài)和離開狀態(tài)時都可能完成相關(guān)操作。根據(jù)SCADE的這些特點，安全狀態(tài)機能夠描述復(fù)雜系統(tǒng)的邏輯結(jié)構(gòu)，確保模型的確定性。對控制結(jié)構(gòu)豐富而數(shù)據(jù)處理較少的模型，十分適合使用安全狀態(tài)機。

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

圖4 SCADE ZC列車管理功能安全狀態(tài)機圖

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

2.2 數(shù)據(jù)流圖

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

表1 列車管理功能狀態(tài)機圖的狀態(tài)含義

ZC 折反請求的 SCADE 數(shù)據(jù)流圖如圖 5所示，當(dāng) ZC 獲取列車狀態(tài)運算符 GetTrainState 解析到列車信息 I_Train_Info 為折返列車 REVERSE_TRAIN并且獲取進路類型運算符 GetRouteType 解析到進路信息 I_RoutInfo 為折返進路 REVERSE_ROUTE 時，觸發(fā)折返轉(zhuǎn)移 T_M2R，列車將進入折返狀態(tài)。

圖5 折返條件數(shù)據(jù)流圖

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

3 模型驗證

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

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

3.1 模擬仿真

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

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

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

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

3.2 模型測試覆蓋率MTC

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

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

3.3 形式化驗證

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

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

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

3.3.1 提取安全屬性

表2 形式驗證與模擬仿真的區(qū)別

安全屬性為保證系統(tǒng)不會發(fā)生危險的屬性，如“CBTC 系統(tǒng)中，列車不能越過 MA 停車”。安全屬性一般來自于設(shè)計規(guī)范及需求等。

3.3.2 方式的轉(zhuǎn)換

建立安全特征觀察器 Observer，即在形式化驗證器中用數(shù)據(jù)流圖的方式將安全需求轉(zhuǎn)換為圖形表達。Observer本質(zhì)上也是 SCADE 的節(jié)點 ,但是多了一些特定的驗證運算符，而且輸出始終為一 Boolean變量且應(yīng)當(dāng)為 true。

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

3.3.3 驗證安全屬性

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

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

圖6 形式驗證過程

圖7 安全特征觀察器模型

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

4 目標(biāo)代碼

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

圖8 KCG模型

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

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

4.1 圖形模型轉(zhuǎn)換為Lustre語言

將節(jié)點、狀態(tài)圖等圖形元素轉(zhuǎn)換成 Lustre 語言描述的模型，并將多個文件模型整合到一個文件中。

4.2 Lustre語言轉(zhuǎn)換為目標(biāo)語言

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

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

5 結(jié)束語

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

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

[1] 張 路 .基于 SCADE 的 CBTC 區(qū)域控制器軟件開發(fā) [D].北京：北京交通大學(xué)，2010.

[2] 高 霖 .CBTC 區(qū)域控制系統(tǒng)中列車管理的建模與分析 [D].北京：北京交通大學(xué)，2007.

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

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

責(zé)任編輯 徐侃春

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

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