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

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

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

0 引 言

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

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

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

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

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

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

圖1 SCADE開(kāi)發(fā)流程

1.2 模型建立

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

數(shù)據(jù)流圖通過(guò)用戶定義的輸入變量接收外界信號(hào)，經(jīng)過(guò)模型處理，再以用戶定義的輸出變量為接口輸出給執(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)前樓層時(shí)，電梯處于上升狀態(tài)；當(dāng)目標(biāo)樓層小于當(dāng)前樓層時(shí)，電梯處于下降狀態(tài)；當(dāng)目標(biāo)樓層相等當(dāng)前樓層時(shí)，電梯處于停止?fàn)顟B(tài)。

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

1.3 模型驗(yàn)證

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

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

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

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

1.4 目標(biāo)代碼

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

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

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

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

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

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

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

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

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

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

3 解決方案

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

（1）安全特性屬性提取錯(cuò)誤；

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

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

安全特性一般是對(duì)系統(tǒng)狀態(tài)或性質(zhì)的要求，通?？梢杂眠壿嬅枋龅姆绞叫问交硎觯赟CADE中以安全特性觀察器模型表述。如電梯的安全特性 “電梯移動(dòng)時(shí)，電梯門(mén)不能處于開(kāi)門(mén)狀態(tài)；電梯門(mén)處于開(kāi)門(mén)狀態(tài)時(shí)，電梯不能移動(dòng)”。電梯移動(dòng)包括上升和下降兩種情況，以A表示電梯上升，B表示電梯下降，C表示電梯門(mén)打開(kāi)。此安全特性可以表示為的邏輯形式，即和C不能同時(shí)為真，安全特性觀察器模型如圖5所示。

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

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

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

圖6 解決方案

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

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

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

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

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

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

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

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

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

4 案例分析

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

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

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

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

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

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

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

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

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

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

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

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

（1）以A表示控制信號(hào)開(kāi)放；

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

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

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

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

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

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

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

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

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

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

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

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

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

經(jīng)過(guò)語(yǔ)法、語(yǔ)義檢測(cè)后，由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)信號(hào) Attestation是否等于Got狀態(tài)，表示收到確認(rèn)信號(hào)，以E表示；＿L22表示控制信號(hào)開(kāi)放且模型處于正常狀態(tài)，以A∧B表示；＿L16表示調(diào)試信號(hào)開(kāi)放，以C表示；inC－＞Communication＿Data＝＝ ＿L11表示通信數(shù)據(jù)為－1，以D表示；＿L11＝＝inC－＞Temp＿Data表示臨時(shí)數(shù)據(jù)為－1，以F表示。outC－＞ValidateOut是安全特性觀察器模型的輸出信號(hào)，通過(guò)C代碼的特點(diǎn)，outC－＞ValidateOut的邏輯結(jié)構(gòu)可表示為

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

5 結(jié)束語(yǔ)

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

：

［1］LU Minyan.Software reliability engineering ［M］.Beijing：National Defense Industry Press，2010 （in Chinese）. ［盧敏燕.軟件可靠性工程 ［M］.北京：國(guó)防工業(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的無(wú)人機(jī)飛行控制軟件設(shè)計(jì) ［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ū)域控制器軟件測(cè)試方法研究 ［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平臺(tái)下的圖形化設(shè)計(jì)和代碼自動(dòng)生成 ［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ū)域控制器軟件開(kāi)發(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軟件開(kāi)發(fā)方法研究 ［J］.系統(tǒng)仿真學(xué)報(bào)，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］.測(cè)控技術(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ì)算機(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對(duì)SCADE開(kāi)發(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的無(wú)人機(jī)飛行控制系統(tǒng)軟件設(shè)計(jì) ［D］.南京：南京航空航天大學(xué)，2008.］

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