基于SCADE的形式化驗(yàn)證技術(shù)的改進(jìn)研究

李 耀，郭 進(jìn)，孔令晶，宋海權(quán)

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

0 引 言

安全苛求系統(tǒng) （safety critical system）是指對安全負(fù)有直接責(zé)任的系統(tǒng)，一旦出現(xiàn)差錯會造成人員傷亡，大宗的財產(chǎn)損失或嚴(yán)重的環(huán)境破壞等災(zāi)難性后果。隨著計算機(jī)技術(shù)的快速發(fā)展，軟件在安全苛求系統(tǒng)中承擔(dān)的功能越來越多，重要性急劇上升。然而隨著軟件規(guī)模及復(fù)雜度的增加，軟件缺陷密度呈幾何級數(shù)增長，失效問題越來越多［1］。近半個世紀(jì)，安全苛求系統(tǒng)由于軟件問題造成的損失幾乎難以估量。在最短的時間內(nèi)開發(fā)出高質(zhì)量的安全軟件已經(jīng)成為一個十分重大的挑戰(zhàn)，傳統(tǒng)的軟件開發(fā)方式已經(jīng)不能滿足需求，SCADE開發(fā)應(yīng)運(yùn)而生。

SCADE （safety critical application development environment），高安全性應(yīng)用開發(fā)環(huán)境，是法國愛斯特爾技術(shù)公司運(yùn)用基于模型的方式為高安全性系統(tǒng)提供的完整的解決方案，能自動生成滿足安全特性的嵌入式代碼，在航空、航天、國防以及核工業(yè)等安全苛求領(lǐng)域得到了廣泛的應(yīng)用。目前，在空中客車，安薩爾多，歐洲直升機(jī)等公司，SCADE開發(fā)方式都有成功案例。其中，空中客車在開發(fā)A340／500－600機(jī)型的飛行控制系統(tǒng)中自動生成了17萬行代碼，總體開發(fā)成本節(jié)約了50%。國內(nèi)在航空和鐵路信號等領(lǐng)域也積累了很多經(jīng)驗(yàn)。形式化驗(yàn)證是SCADE的核心功能之一，在保證軟件安全過程中具有不可替代的作用。但SCADE形式化驗(yàn)證模型中的安全特性觀察器的正確性一直依靠設(shè)計者的經(jīng)驗(yàn)保障，缺乏驗(yàn)證方式，本文利用SCADE開發(fā)的特點(diǎn)，對此問題提出了一種解決方案。

1 SCADE開發(fā)基礎(chǔ)

1.1 SCADE開發(fā)的特點(diǎn)

SCADE基于同步編程理論，以Lustre語言為核心，覆蓋了從需求到代碼的所有開發(fā)流程，包括需求管理、需求建模、模型檢查、模擬仿真、測試覆蓋率分析、形式化驗(yàn)證、代碼生成、文檔生成等［2］。SCADE開發(fā)解決了傳統(tǒng)開發(fā)的很多不足［3］，傳統(tǒng)開發(fā)方式工作量大，效率低，投入高，驗(yàn)證難，設(shè)計可能存在歧義，維護(hù)及升級復(fù)雜；而SCADE開發(fā)十分方便，具有開發(fā)質(zhì)量好、效率高，成本低、風(fēng)險小、驗(yàn)證時間短，能夠保證軟件質(zhì)量等優(yōu)點(diǎn)，從傳統(tǒng)的以 “代碼”為核心轉(zhuǎn)變?yōu)橐?“模型”為核心，避免手工編碼，開發(fā)人員關(guān)注軟件需求的正確性，體現(xiàn)了軟件設(shè)計的真正意義。

SCADE具有嚴(yán)格的數(shù)學(xué)語義，運(yùn)用了Correct By Construction的設(shè)計理念，能夠在軟件開發(fā)初期清除系統(tǒng)的模糊性和二義性，由精確的需求規(guī)范自動生成嵌入式代碼，實(shí)現(xiàn)了開發(fā)流程的高度自動化，確保軟件的可靠性、安全性。SCADE使用編輯器嚴(yán)格準(zhǔn)確地對需求進(jìn)行建模，自動檢查需求的安全性、完整性、一致性，通過仿真器和設(shè)計驗(yàn)證器保障模型安全的需求，最后由代碼生成器自動生成面向工程的目標(biāo)代碼，整個開發(fā)過程具有可追蹤性，開發(fā)流程如圖1所示。

圖1 SCADE開發(fā)流程

1.2 模型建立

建模是SCADE對需求的一種準(zhǔn)確、無歧義的圖形化表達(dá)，是SCADE開發(fā)的基礎(chǔ)。SCADE支持?jǐn)?shù)據(jù)流圖和安全狀態(tài)機(jī)兩種圖形方式建模。安全狀態(tài)機(jī)常常用于描述離散系統(tǒng)的狀態(tài)及邏輯結(jié)構(gòu)，而數(shù)據(jù)流圖善于描述數(shù)據(jù)的處理過程，反應(yīng)時序及因果關(guān)系，常常用于連續(xù)系統(tǒng)的建模。

數(shù)據(jù)流圖通過用戶定義的輸入變量接收外界信號，經(jīng)過模型處理，再以用戶定義的輸出變量為接口輸出給執(zhí)行機(jī)構(gòu)。圖2為電梯運(yùn)行方向的數(shù)據(jù)流圖。

圖2 電梯運(yùn)行方向數(shù)據(jù)流

圖2中，Des＿Floor表示用戶輸入的目標(biāo)樓層，Cur－rent＿Floor表示電梯當(dāng)前所處的樓層。數(shù)據(jù)流圖表示：當(dāng)目標(biāo)樓層大于當(dāng)前樓層時，電梯處于上升狀態(tài)；當(dāng)目標(biāo)樓層小于當(dāng)前樓層時，電梯處于下降狀態(tài)；當(dāng)目標(biāo)樓層相等當(dāng)前樓層時，電梯處于停止?fàn)顟B(tài)。

數(shù)據(jù)流圖和安全狀態(tài)機(jī)都建立在嚴(yán)格的數(shù)學(xué)模型基礎(chǔ)之上，具有嚴(yán)格的數(shù)學(xué)語義，保證了設(shè)計模型的精確性、完整性、一致性和無二義性。SCADE把兩套機(jī)制很好的結(jié)合在一起，能夠適合不同類型的系統(tǒng)尤其是混合系統(tǒng)的開發(fā)。

1.3 模型驗(yàn)證

SCADE提供模擬仿真和形式化驗(yàn)證兩種方式保障模型安全。一般，在系統(tǒng)開發(fā)早期使用模擬仿真，而在設(shè)計的最后階段使用形式化驗(yàn)證。

模擬仿真通過觀察模型對指定輸入的響應(yīng)行為判斷設(shè)計是否符合預(yù)期需求，但不能保證模型滿足所有的安全性要求，無法證明模型無錯誤，SCADE提供形式化驗(yàn)證彌補(bǔ)此不足。

形式化驗(yàn)證通過數(shù)學(xué)推理對系統(tǒng)做詳盡的分析，具有完備性的優(yōu)點(diǎn)，不需要任何測試用例，是保障模型安全的重要方法。SCADE形式化驗(yàn)證首先需要在設(shè)計驗(yàn)證器中建立安全特性觀察器模型Observe。Observer是安全特性屬性在SCADE中的圖形形式化表達(dá)，其輸出始終為一Bool變量，且應(yīng)當(dāng)為true。設(shè)計驗(yàn)證器連接待驗(yàn)證的設(shè)計模型Design和Observer模型，持續(xù)檢測待驗(yàn)證模型的輸入、輸出信號，證明在所有周期及所有可能的場景下Observer都是正確的，如圖3所示。

圖3 形式化驗(yàn)證模型

1.4 目標(biāo)代碼

SCADE開發(fā)的最終目標(biāo)是生成可信代碼。SCADE代碼生成器 KCG通過了 DO－178BA 級、IEC 61508SIL3、EN 50128 3／4和IEC 60880的認(rèn)證，以模型作為輸入，根據(jù)用戶設(shè)定的參數(shù)，自動生成面向工程且滿足安全特性的ANSI C或 Ada代碼和可跟蹤文件［4］。

KCG對使用數(shù)據(jù)流圖方式建立的邏輯結(jié)構(gòu)，生成的代碼仍然保持了邏輯結(jié)構(gòu)的特點(diǎn)。如A＋B＞0，KCG生成代碼如下：

2 SCADE形式化驗(yàn)證的不足

SCADE形式化驗(yàn)證流程如下：

（1）提取安全特性屬性。安全特性屬性是保證系統(tǒng)不會發(fā)生危險的屬性，一般來自軟件需求或安全性標(biāo)準(zhǔn)等，如 “電梯移動過程中不能打開電梯門”；

（2）建立安全特性觀察器模型，將安全特性需求轉(zhuǎn)換為圖形表達(dá)；

（3）驗(yàn)證安全特性屬性。SCADE整合待驗(yàn)證模型和安全特性觀察器模型，自動驗(yàn)證系統(tǒng)是否滿足安全需求，如果發(fā)現(xiàn)沖突，安全特性觀察器模型輸出false警報信號，同時給出反例；否則輸出true，給出安全證明，如圖4所示。

提取安全特性屬性和建立安全特性觀察器模型由人工完成，對設(shè)計者的專業(yè)知識及技能有一定的要求。安全特性觀察器模型的正確性關(guān)系到驗(yàn)證結(jié)果的有效性，但SCADE不能檢測安全特性觀察器模型的正確性，無法驗(yàn)證模型是否正確表達(dá)了設(shè)計者的意圖。

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

對于模擬仿真，由于測試向量的數(shù)量關(guān)系到仿真的完備程度，SCADE提供模型測試覆蓋率MTC定量分析仿真的完備程度。模擬仿真是對模型的驗(yàn)證，MTC是對模擬仿真的驗(yàn)證，是驗(yàn)證的驗(yàn)證。而對形式化驗(yàn)證，SCADE未提供類似的驗(yàn)證方法，安全特性觀察器的正確性缺乏判斷依據(jù)，完全依靠設(shè)計者的經(jīng)驗(yàn)保障。形式化驗(yàn)證是保障模型正確性、安全性廣泛使用的重要方法，安全特性觀察器是SCADE形式化驗(yàn)證的核心模型，其正確性關(guān)系到軟件的安全性。如果安全特性觀察器模型建立錯誤，設(shè)計驗(yàn)證器將以錯誤的觀察器模型驗(yàn)證系統(tǒng)，軟件中的故障可能沒有被檢測，潛伏在系統(tǒng)中，在一些特定的環(huán)境下暴露并帶來災(zāi)難性的危害，這在安全苛求系統(tǒng)中是不容許的。

3 解決方案

安全特性觀察器建立錯誤一般有兩種情況：

（1）安全特性屬性提取錯誤；

（2）安全特性觀察器模型建立錯誤。

第一種錯誤一般是由于設(shè)計人員對系統(tǒng)的安全特性或需求理解錯誤造成的，在實(shí)際開發(fā)中，由于設(shè)計人員的專業(yè)能力較強(qiáng)，此種錯誤相對較少。第二種錯誤是指設(shè)計人員對安全特征理解正確，但建立安全特性觀察器模型出現(xiàn)錯誤，所建模型完成的功能和預(yù)期功能不一致，偏離了設(shè)計者的本意，在安全特征較為復(fù)雜時該種情況尤為常見。本文針對第二種錯誤提出一種驗(yàn)證方法。

安全特性一般是對系統(tǒng)狀態(tài)或性質(zhì)的要求，通常可以用邏輯描述的方式形式化表述，在SCADE中以安全特性觀察器模型表述。如電梯的安全特性 “電梯移動時，電梯門不能處于開門狀態(tài)；電梯門處于開門狀態(tài)時，電梯不能移動”。電梯移動包括上升和下降兩種情況，以A表示電梯上升，B表示電梯下降，C表示電梯門打開。此安全特性可以表示為的邏輯形式，即和C不能同時為真，安全特性觀察器模型如圖5所示。

圖5 電梯安全特性觀察器模型

安全特性觀察器本質(zhì)上也是SCADE的節(jié)點(diǎn)，只是多了一些特定的驗(yàn)證運(yùn)算符，但驗(yàn)證運(yùn)算符可以在編輯器中設(shè)計。圖3是在編輯器中描述電梯的移動狀態(tài)，圖5是在設(shè)計驗(yàn)證器中描述電梯的安全特性需求，兩者采用的都是數(shù)據(jù)流圖，本質(zhì)相同，所以設(shè)計驗(yàn)證器中的安全特性觀察器模型可以移植到編輯器中。在編輯器中建立的安全特性觀察器模型同編輯器中的其他模型一樣，可以模擬仿真，形式化驗(yàn)證和用KCG生成代碼，比在設(shè)計驗(yàn)證器中擁有更多的驗(yàn)證方式。

通過以上的分析，安全特性屬性可以用邏輯描述的方式形式化表示，KCG對邏輯結(jié)構(gòu)的模型生成的可信代碼保持了邏輯特征，所以在編輯器中完成安全特性觀察器模型后，通過KCG生成C代碼，安全特性觀察器模型轉(zhuǎn)化為了C代碼表現(xiàn)形式，即安全特性屬性轉(zhuǎn)化為了C代碼表現(xiàn)形式。通過比較C代碼的邏輯結(jié)構(gòu)和安全特性屬性的邏輯描述的結(jié)構(gòu)，可以驗(yàn)證安全特性觀察器模型是否實(shí)現(xiàn)預(yù)期功能，如圖6所示。

圖6 解決方案

改進(jìn)后，SCADE形式化驗(yàn)證流程如下：

（1）提取安全特性屬性；

（2）將安全特性屬性抽象為邏輯形式，復(fù)雜表達(dá)式可以化簡；

（3）在編輯器中使用數(shù)據(jù)流圖方式對安全特性屬性建模；

（4）根據(jù)安全特性屬性的特點(diǎn)，可以使用仿真或形式化驗(yàn)證方式驗(yàn)證安全特性觀察器模型；

（5）使用KCG生成C代碼；

（6）比較步驟2抽象的邏輯形式和C代碼邏輯結(jié)構(gòu)是否一致，不一致表明安全特性觀察器模型建立錯誤，返回步驟3完善模型；

（7）將安全特性觀察器模型移植到設(shè)計驗(yàn)證器中，同常規(guī)驗(yàn)證流程繼續(xù)驗(yàn)證，如圖7所示。

圖7 改進(jìn)后的驗(yàn)證流程

4 案例分析

某系統(tǒng)由A、B、C這3個模塊組成，模塊B完成核心計算功能，A為B提供運(yùn)行所需的控制信息，包括控制信號、狀態(tài)信息、調(diào)試信號，其中狀態(tài)信息包括正常狀態(tài)和故障狀態(tài)；C為B提供數(shù)據(jù)，包括通信數(shù)據(jù)和臨時數(shù)據(jù)，如圖8所示。

系統(tǒng)運(yùn)行時，模塊A的輸出信息必須滿足以下安全需求：

圖8 系統(tǒng)結(jié)構(gòu)

（1）控制信號開放且狀態(tài)信息為正常狀態(tài)；

（2）或控制信號關(guān)閉且調(diào)試信號開放；

（3）或狀態(tài)信息為故障狀態(tài)且調(diào)試信號開放；

（4）“控制信號開放且狀態(tài)信息處于正常狀態(tài)”不能與“調(diào)試信號開放”同時出現(xiàn)。

模塊C的輸出數(shù)據(jù)必須滿足以下安全需求：

（1）接收到的通信數(shù)據(jù)不為 “－1”且收到確認(rèn)信號；

（2）或接收到的臨時數(shù)據(jù)不為 “－1”且收到確認(rèn)信號；

（3）或接收的通信數(shù)據(jù)為 “－1”且臨時數(shù)據(jù)為 “－1”。

以上為系統(tǒng)的安全需求，為以邏輯形式準(zhǔn)確、無歧義表達(dá)安全特性，做如下約定：

（1）以A表示控制信號開放；

（2）以B表示狀態(tài)信息處于正常狀態(tài)；

（3）以C表示調(diào)試信號開放；

（4）以D表示通信數(shù)據(jù)為 “－1”；

（5）以E表示模塊C收到數(shù)據(jù)確認(rèn)信號；

（6）以F表示臨時數(shù)據(jù)為 “－1”；

基于以上約定，系統(tǒng)的安全需求可以抽象為如下邏輯形式

（A∧B∨瓙A∧C∨瓙B∧C）（瓙（A∧B∧C））（瓙D∧E∨瓙F∧E∨D∧F）

通過邏輯運(yùn)算，安全特性需求可以等價簡化為：

（A∧B∨C）（瓙（A∧B∧C））（E∨D∧F）

在編輯器中對化簡前后的安全特性屬性建立安全特性觀察器模型，如圖9所示。

圖9 系統(tǒng)安全特性觀察器模型

圖9（a）、圖9（b）分別為簡化前后的安全特性觀察器模型，兩者功能相同，但模型圖9（b）結(jié)構(gòu)更清晰，層次更清楚，相對簡單，建模不容易出錯，減小了驗(yàn)證失敗的概率。模型圖9（a）、圖9（b）并未直接實(shí)現(xiàn)系統(tǒng)需要的安全特性，期望模型的輸入并不是A、B、C等信息，而是控制信號、狀態(tài)信息等系統(tǒng)信息。在模型中將邏輯常量A、B、C、D、E、F分別轉(zhuǎn)換為對應(yīng)的系統(tǒng)信息，建立系統(tǒng)的安全特性觀察器模型如圖10所示。

圖10 系統(tǒng)安全特性觀察器模型

經(jīng)過語法、語義檢測后，由KCG生成C代碼，驗(yàn)證所建立的模型是否實(shí)現(xiàn)了預(yù)期的期望。圖10所示模型生成的C代碼如圖11所示。

圖11 系統(tǒng)安全特性模型C代碼

函數(shù)kcg＿comp＿array＿char＿＊比較參數(shù)是否一致，如kcg＿comp＿array＿char＿3 （＆inC－＞Attestation，（array＿char＿3＊）＆States.Got）比較確認(rèn)信號 Attestation是否等于Got狀態(tài)，表示收到確認(rèn)信號，以E表示；＿L22表示控制信號開放且模型處于正常狀態(tài)，以A∧B表示；＿L16表示調(diào)試信號開放，以C表示；inC－＞Communication＿Data＝＝ ＿L11表示通信數(shù)據(jù)為－1，以D表示；＿L11＝＝inC－＞Temp＿Data表示臨時數(shù)據(jù)為－1，以F表示。outC－＞ValidateOut是安全特性觀察器模型的輸出信號，通過C代碼的特點(diǎn)，outC－＞ValidateOut的邏輯結(jié)構(gòu)可表示為

此邏輯結(jié)構(gòu)和簡化后的安全特性需求的邏輯結(jié)構(gòu)完全一致，說明安全特性觀察器模型完成預(yù)期功能，模型建立正確，可移植到設(shè)計驗(yàn)證器中完成系統(tǒng)驗(yàn)證。

5 結(jié)束語

本文在充分研究利用SCADE開發(fā)特點(diǎn)的基礎(chǔ)上，利用編輯器和代碼生成器的特點(diǎn)，使用邏輯描述的方式形式化描述安全特性屬性，對SCADE形式化驗(yàn)證中安全特性觀察器模型的正確性提出了一種驗(yàn)證方法，改進(jìn)了SCADE形式化驗(yàn)證技術(shù)，能夠有效的檢驗(yàn)安全特性觀察器模型的正確性，保證模型安全，降低模型檢驗(yàn)中人的主觀性，在實(shí)際應(yīng)用中取得一定效果，對安全苛求系統(tǒng)軟件開發(fā)有一定的現(xiàn)實(shí)意義和實(shí)用價值。但對于復(fù)雜的模型，特別是使用了設(shè)計驗(yàn)證運(yùn)算符的模型，此方法有一定的困難，下一步的研究將嘗試自動生成邏輯描述表達(dá)式，自動完成驗(yàn)證。

：

［1］LU Minyan.Software reliability engineering ［M］.Beijing：National Defense Industry Press，2010 （in Chinese）. ［盧敏燕.軟件可靠性工程 ［M］.北京：國防工業(yè)出版社，2010.］

［2］YAN Wenqing.The software design of flight control system for UAV based on SCADE ［D］.Nanjing：Nanjing University of Aeronautics and Astronautics，2008 （in Chinese）.［顏雯清.基于SCADE的無人機(jī)飛行控制軟件設(shè)計 ［D］.南京：南京航空航天大學(xué)，2008.］

［3］LI Lei.Research on software testing method of CBTC zone controller based on SCADE ［D］.Beijing：Beijing Jiaotong University，2010 （in Chinese）.［李雷.基于SCADE的 CBTC區(qū)域控制器軟件測試方法研究 ［D］.北京：北京交通大學(xué)，2010.］

［4］ZHANG Xiaochun，JIN Ping，SUN Quanyan.Modeling and autogeneration of C code on SCADE bench［J］.Software，2011，32 （5）：74－77 （in Chinese）.［章 曉 春， 金 平， 孫 全 艷.SCADE平臺下的圖形化設(shè)計和代碼自動生成 ［J］.軟件，2011，32 （5）：74－77.］

［5］ZHANG Lu.SCADE supported software development of zone controller in CBTC system ［D］.Beijing：Beijing Jiaotong University，2010 （in Chinese）.［張路.基于SCADE的CBTC區(qū)域控制器軟件開發(fā) ［D］.北京：北京交通大學(xué)，2010.］

［6］HU Gangwei，LI Zhenshui，GAO Yakui.A research on software development methods with SCADE ［J］.Journal of System Simulation.2009，20 （Suppl）：286－288 （in Chinese）.［胡鋼偉，李振水，高亞奎.SCADE軟件開發(fā)方法研究 ［J］.系統(tǒng)仿真學(xué)報，2009，20 （Suppl）：286－288.］

［7］LIN Feng.Research on SCADE－based formal verification technology［J］.Measurement ＆ Control Technology，2011，30（12）：71－74 （in Chinese）.［林楓.基于SCADE的形式化驗(yàn)證技術(shù)研究 ［J］.測控技術(shù)，2011，30 （12）：71－74.］

［8］LIN Feng.Implementation of trigonometric function by SCADE suite［J］.Computer Systems ＆ Applications，2012，21 （3）：228－231 （in Chinese）.［林楓.三角函數(shù)的SCADE Suite實(shí)現(xiàn)方法 ［J］.計算機(jī)系統(tǒng)應(yīng)用，2012，21 （3）：228－231.］

［9］ZHOU Jiaming.Formal modeling and verification for the rail transit control system designed by SCADE base on PVS ［D］.Shanghai：East China Normal University，2011 （in Chinese）.［周佳銘.基于PVS對SCADE開發(fā)軌交控制系統(tǒng)的形式化建模與驗(yàn)證 ［D］.上海：華東師范大學(xué)，2011.］

［10］WANG Xin.Based on SCADE the software design of flight control system for UAV ［D］.Nanjing：Nanjing University of Aeronautics and Astronautics，2008 （in Chinese）.［王鑫.基于SCADE的無人機(jī)飛行控制系統(tǒng)軟件設(shè)計 ［D］.南京：南京航空航天大學(xué)，2008.］

［11］ESTEREL Technologies.SCADE suite.［EB／OL］.［2012－11－01］.http：／／www.esterel－technologies.com／products／scade－suite／／.