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

陳淑珍，陳榮武，李 耀

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

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

陳淑珍，陳榮武，李 耀

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

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

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

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

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

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

1 理論基礎(chǔ)

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

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

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

1.2 同步假設(shè)

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

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

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

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

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

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

1.3 Lustre

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

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

（1）初始顯示 0；

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

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

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

圖2 計(jì)數(shù)器Lustre表達(dá)1

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

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

圖3 計(jì)數(shù)器Lustre表達(dá)2

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

2 模型建立

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

2.1 安全狀態(tài)機(jī)

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

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

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

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

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

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

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

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

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

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

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

3 模型驗(yàn)證

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

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

3.1 模擬仿真

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

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

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

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

3.2 模型測(cè)試覆蓋率MTC

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

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

3.3 形式化驗(yàn)證

SCADE 提供形式化驗(yàn)證的方式保證安全需求。

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

SCADE 形式化驗(yàn)證與仿真測(cè)試，如表 2所示。

3.3.1 提取安全屬性

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

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

3.3.2 方式的轉(zhuǎn)換

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

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

3.3.3 驗(yàn)證安全屬性

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

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

圖6 形式驗(yàn)證過程

圖7 安全特征觀察器模型

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

4 目標(biāo)代碼

SCADE 開發(fā)的最終目標(biāo)就是生成可信代碼。SCADE 的代碼生成器 KCG 通過了 DO-178B A 級(jí)、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)信息，并進(jìn)行語法語義檢查；中間模塊是編譯核心和優(yōu)化器；后端模塊生成目標(biāo)代碼和可追蹤文件[5]。

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

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

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

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

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

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

5 結(jié)束語

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

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

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

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

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

[4] 林 楓 .基于 SCADE 的形式化驗(yàn)證技術(shù)研究 [J].測(cè)控技 術(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

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