張 漾，胡 軍，王立松，康介祥，王 輝，高忠杰

1(南京航空航天大學(xué) 計(jì)算機(jī)科學(xué)與技術(shù)學(xué)院，南京 211106)2(軟件新技術(shù)與產(chǎn)業(yè)化協(xié)同創(chuàng)新中心，南京 210007)3(中國(guó)航空無線電電子研究所，上海 200233)

1 引 言

計(jì)算機(jī)系統(tǒng)軟件本身的可靠性和安全性是安全關(guān)鍵系統(tǒng)[1，2]正常運(yùn)行的先決條件.近年來航空事業(yè)發(fā)展迅速，航電系統(tǒng)[3]的復(fù)雜性急劇增加，機(jī)載軟件適航認(rèn)證標(biāo)準(zhǔn)DO-178C[4]支持采用形式化方法驗(yàn)證航空軟件.基于模型的安全評(píng)估[5，6](MBSA)方法可以通過對(duì)安全關(guān)鍵系統(tǒng)建立模型，從而將復(fù)雜的系統(tǒng)行為描述為精確的、可讀的數(shù)學(xué)表達(dá)式，并對(duì)相關(guān)需求規(guī)約[7，8]實(shí)現(xiàn)分析，檢查需求模型的一致性和完備性，驗(yàn)證系統(tǒng)的正確性.

T-VEC是基于4變量模型[9，10]中的SCR方法，進(jìn)行需求設(shè)計(jì)、需求建模的工具.通過表格表達(dá)式，它用模式轉(zhuǎn)換表、條件表和事件表等形式化數(shù)學(xué)符號(hào)，描述系統(tǒng)在不同的模式、條件和狀態(tài)下，狀態(tài)變量不同的取值，表現(xiàn)系統(tǒng)狀態(tài)遷移的邏輯關(guān)系，從而實(shí)現(xiàn)對(duì)系統(tǒng)行為形式化描述.

形式化驗(yàn)證[11]是用精確的、高效的數(shù)學(xué)方法驗(yàn)證系統(tǒng)的正確性或評(píng)估系統(tǒng)可能存在的缺陷，從而做出關(guān)于系統(tǒng)設(shè)計(jì)的正確決策.形式化方法有3大類分別是演繹證明(deductive proof)、模型檢驗(yàn)(model checking)和抽象解釋(abstract interpretation).本文主要介紹和使用在工業(yè)上應(yīng)用最廣泛的模型檢驗(yàn)方法.模型檢驗(yàn)[12]是一種自動(dòng)化驗(yàn)證技術(shù)，其輸入是描述成狀態(tài)機(jī)的系統(tǒng)模型和描述成模態(tài)邏輯公式的待驗(yàn)證系統(tǒng)屬性，通過驗(yàn)證“模型狀態(tài)機(jī)可達(dá)路徑是否滿足模態(tài)邏輯公式”來給出結(jié)果；其輸出是滿足系統(tǒng)性質(zhì)的肯定反饋或不滿足系統(tǒng)性質(zhì)的反例.時(shí)態(tài)邏輯[13](temporal logic)是計(jì)算機(jī)形式化研究中重要的分支，其將系統(tǒng)結(jié)構(gòu)中所有的狀態(tài)可達(dá)關(guān)系解釋為基于時(shí)間的先后次序關(guān)系.本文主要將系統(tǒng)的動(dòng)態(tài)待驗(yàn)證屬性的狀態(tài)集描述為形式化規(guī)約，轉(zhuǎn)換成可執(zhí)行、無二義的線性時(shí)序邏輯(Linear-time Temporal Logic，LTL)和計(jì)算樹時(shí)序邏輯(Computation Tree Logic，CTL)公式，將其作為標(biāo)準(zhǔn)的模型檢驗(yàn)輸入.

nuXmv[14-16]是一種傳統(tǒng)的符號(hào)化模型檢測(cè)器.nuXmv是SMV擴(kuò)展而來的，SMV最早是由卡內(nèi)基梅隆大學(xué)的K.L.McMillan研發(fā)，是第1個(gè)基于BDD的模型檢查器.之后，經(jīng)由功能擴(kuò)展和重新實(shí)現(xiàn)的nuXmv加入了基于SAT算法的驗(yàn)證引擎，能夠?qū)τ邢逘顟B(tài)和無限狀態(tài)的系統(tǒng)進(jìn)行形式化驗(yàn)證.nuXmv的模型建模語言XMV通過對(duì)有限狀態(tài)自動(dòng)機(jī)[17]Finite State Machine(FSM)和無限狀態(tài)系統(tǒng)的狀態(tài)轉(zhuǎn)換的描述對(duì)系統(tǒng)建模，用狀態(tài)遷移定義事件觸發(fā)下的系統(tǒng)變量取值的改變.

本文將T-VEC語言定義的表格關(guān)系模型轉(zhuǎn)換為自動(dòng)機(jī)狀態(tài)遷移圖，再將狀態(tài)圖解釋為nuXmv可以理解的符號(hào)化模型檢測(cè)語言XMV，進(jìn)而為建模后的安全關(guān)鍵系統(tǒng)軟件檢查需求的一致性與完備性.基于ANTLR4語法解析工具，本文提出和實(shí)現(xiàn)了一種模型變量關(guān)系平展簡(jiǎn)化的方法，解決了T-VEC建模語言語法結(jié)構(gòu)上的遞歸定義問題，完成了模型轉(zhuǎn)換及狀態(tài)圖解釋工具的開發(fā).本文第2節(jié)對(duì)T-VEC和nuXmv模型進(jìn)行形式化定義；第3節(jié)對(duì)SCR模型系統(tǒng)驗(yàn)證框架進(jìn)行闡述；第4節(jié)對(duì)模型變量關(guān)系平展簡(jiǎn)化方法進(jìn)行具體說明；第5節(jié)對(duì)模型轉(zhuǎn)換規(guī)則進(jìn)行定義并給出正確性證明；第6節(jié)對(duì)飛行引導(dǎo)系統(tǒng)(Flight Guidance System，F(xiàn)GS)進(jìn)行分析，最后對(duì)本文相關(guān)工作進(jìn)行總結(jié)，對(duì)未來應(yīng)用進(jìn)行展望.

2 T-VEC與nuXmv模型

2.1 T-VEC語義

T-VEC語言定義了以需求為中心，以表格表達(dá)式表示的系統(tǒng)模型形式，其將模型保存為以.SS為后綴的文件格式.為了方便，下文中均將T-VEC抽象需求模型稱為SS模型.每一個(gè)SS模型都包含多個(gè)SS文件，每一個(gè)帶有約束的和正向輸出的中間變量和輸出變量都保存為一個(gè).SS文件.其中，每一個(gè).SS文件包含了一個(gè)系統(tǒng)定義變量和多條系統(tǒng)控制約束語句，針對(duì)不同的系統(tǒng)控制約束，系統(tǒng)定義變量有不同的取值.

圖1(a)描述了SS需求模型的文件結(jié)構(gòu)，圖1(b)描述了在該文件結(jié)構(gòu)下的.SS文件組成邏輯.由圖1(a)可見，SS模型的描述語言是一種對(duì)象離散的抽象語言，其沒有順序、循環(huán)等流程控制語句，也沒有復(fù)雜多變的自定義方法和自定義過程.但是在圖1(b)組成邏輯中可以發(fā)現(xiàn)，SS模型的變量結(jié)構(gòu)上存在遞歸定義特征，針對(duì)當(dāng)前的中間、輸出變量，可以引入SS模型中包含的其他中間和輸出變量作為控制約束.

在本節(jié)中，為了精確描述T-VEC語言語義的邏輯，本文使用SS模型擴(kuò)展定義T-VEC的語言(下文中稱為SSM)，給出如下形式化定義：

定義1.一個(gè)SS模型(SSM)是一個(gè)三元組SSM=，其中：

1)T是一個(gè)類型集合，是基本類型TBasic與自定義類型TCustom的并集：T=TBasic∪TCustom.

圖1 SS模型文件結(jié)構(gòu)和組成邏輯Fig.1 SS model′s file structure and file format

2)TBasic是基本類型，其中包含布爾型Boolean、整型Integer、浮點(diǎn)型float/double、字符串型String.

3)TCustom是自定義類型，其中包含3個(gè)字段，分別是類型名稱、原始類型和類型范圍.

4)V是一個(gè)變量集合，是輸入變量Vin、中間變量Vterm和輸出變量Vout的并集：V=Vin∪Vterm∪Vout.

5)Vin是輸入變量，是不參加狀態(tài)遷移的原子變量.

6)Vterm是中間變量，是包含變量約束的復(fù)合變量.

7)Vout是輸出變量，是包含變量約束的復(fù)合變量，用于描述待驗(yàn)證屬性.

8)C是一個(gè)約束集合，是條件約束Ccon和事件約束Cet的并集：C=Ccon∪Cet.

9)Ccon是變量取值笛卡爾積的一個(gè)子集，Ccon?{(V，val)|V∈V×V，val∈TypeRange}其中：V??，val??.

10)Cet帶有時(shí)間屬性的變量取值笛卡爾積的一個(gè)子集Cet?{(VT，val)|VT∈VT×VT，val∈TypeRange}其中：VT??，val??.

事實(shí)上，SS模型包含兩個(gè)配置文件coreRTS.SS和runTimeData.SS，以及多個(gè)中間、輸出變量定義文件.配置文件分別描述了所有基本類型、該基本類型的取值范圍的定義和用戶定義類型與基本類型間的傳遞定義.傳遞定義既提供了變量類型的靈活性，也保證了變量取值范圍的一致性.變量定義文件運(yùn)用了模型中的條件表、事件表、模式類等來描述模型中的狀態(tài)遷移，體現(xiàn)了模型行為的動(dòng)態(tài)性.SS模型包含了輸入變量約束、中間變量約束和輸出變量約束，約束本質(zhì)上是變量與變量取值的選擇，體現(xiàn)的是其他變量取值對(duì)待檢查變量取值的影響，以及對(duì)整個(gè)系統(tǒng)運(yùn)作和狀態(tài)遷移的影響.

2.2 nuXmv語義

nuXmv定義了從系統(tǒng)狀態(tài)出發(fā)，用狀態(tài)遷移描述系統(tǒng)運(yùn)作進(jìn)程的模型形式，其將模型保存為以.SMV為后綴的單個(gè)文件格式.為了方便，下文中均將nuXmv需輸入的抽象需求模型稱為XMV模型.一個(gè)XMV模型由一個(gè)主模塊(MODULE)與若干個(gè)子模塊構(gòu)成，模塊之間由變量參數(shù)關(guān)聯(lián)，子模塊之間可以互相嵌套迭代，可以多次復(fù)用，最后都由主模塊單獨(dú)調(diào)用.與SS模型不同，XMV模型由狀態(tài)驅(qū)動(dòng)，以狀態(tài)的遷移反映模型的動(dòng)態(tài)行為，狀態(tài)由最小單元狀態(tài)變量(VAR)組成.在XMV模型中，用ASSIGN聲明進(jìn)入狀態(tài)轉(zhuǎn)換，定義狀態(tài)變量賦值；用INIT代表新引入的狀態(tài)變量初始賦值；用NEXT代表在當(dāng)前狀態(tài)約束下，下一狀態(tài)的變量取值.

在本節(jié)中，為了精確描述nuXmv語言語義的邏輯，本文使用XMV模型擴(kuò)展定義nuXmv的建模語言，下文中稱為XMV，給出如下形式化定義：

定義2.一個(gè)XMV模型是一個(gè)七元組XMV=，其中：

1)M是一個(gè)模塊(MODULE)的集合，是主模塊Mmain與若干子模塊Mi的并集：M=Mmain∪Mi，其中i=1，2…n.

2)Mi子模塊是狀態(tài)S與狀態(tài)遷移關(guān)系T笛卡爾積的一個(gè)子集Mi?S×TS.

3)S是一個(gè)狀態(tài)的集合，是初始狀態(tài)S0、中間狀態(tài)Si和終結(jié)狀態(tài)F的并集：S=S0∪Si∪F，其中i=1，2…n.

4)S0是模型的初始狀態(tài)，S0∈S，初始狀態(tài)是變量INIT賦值集合.

5)Si是模型的中間狀態(tài)，Si∈S，中間狀態(tài)是變量NEXT賦值集合.

6)V是一個(gè)變量的集合，是輸入變量組IVAR，狀態(tài)變量組VAR和凍結(jié)變量組FROZENVAR的并集，V=IVAR∪VAR∪FROZENVAR.

7)C是狀態(tài)轉(zhuǎn)移約束的集合，此約束可以是觸發(fā)的系統(tǒng)事件或者狀態(tài)推進(jìn)要求滿足某種條件.

8)T是狀態(tài)轉(zhuǎn)移的集合，ti∈T，ti=Si→Si(Si×C×Si)，其中i=1，2…n，ti表示某個(gè)狀態(tài)遷移至另一個(gè)狀態(tài)的過程，其本質(zhì)是兩個(gè)狀態(tài)集與約束集的笛卡爾積.

9)F是終結(jié)狀態(tài)的集合，是狀態(tài)集合的一個(gè)子集：F?S.終結(jié)狀態(tài)不唯一，不同的屬性規(guī)約要求有不同的終結(jié)狀態(tài)，因此F由SPEC決定.

本質(zhì)上，XMV語言由XMV模型和屬性規(guī)約構(gòu)成，其結(jié)構(gòu)由關(guān)鍵字MODULE、ASSIG-N、DEFINE、INVAR、INIT、NEXT、IVAR、VAR、FROZENVAR、SPEC等描述.其中，MODULE是模塊聲明詞，用于聲明主模塊或子模塊，可以自定義名稱和帶有參數(shù)，用于關(guān)系的傳遞；ASSIGN提示了狀態(tài)變量賦值開始，進(jìn)入狀態(tài)轉(zhuǎn)換階段；DEFINE是宏定義關(guān)鍵字，用于抽象預(yù)定義規(guī)則，利用宏名代替命令序列，在下文中，DEFINE主要將約束邏輯序列定義為約束名稱，便于模型中變量根據(jù)條件和事件約束賦值使用；INVAR是定值聲明詞，用于定義系統(tǒng)中的常量；INIT是初始化操作關(guān)鍵字，在狀態(tài)變量賦值開始后可以對(duì)變量初始賦值，組成初始狀態(tài)S0；NEXT是下一狀態(tài)賦值操作關(guān)鍵字，在狀態(tài)變量賦值開始后，在滿足DEFINE描述的特定約束下，可以對(duì)變量進(jìn)行下一狀態(tài)賦值；IVAR是輸入變量聲明詞，用于定義輸入變量，將外界環(huán)境作為變量參數(shù)引入模型，體現(xiàn)環(huán)境的影響；VAR是狀態(tài)變量聲明詞，用于定義狀態(tài)變量，是參與系統(tǒng)狀態(tài)遷移的主要成分，體現(xiàn)系統(tǒng)的運(yùn)作；FROZENVAR是凍結(jié)變量聲明詞，用于定義凍結(jié)變量，凍結(jié)變量沒有賦值改變，保證狀態(tài)穩(wěn)定的變量；SPEC是屬性規(guī)約關(guān)鍵字，使用LTL、CTL和PTL時(shí)序邏輯、變量不變規(guī)約等來描述待驗(yàn)證需求，說明系統(tǒng)性質(zhì).

3 面向SCR模型的系統(tǒng)安全性驗(yàn)證框架

本節(jié)對(duì)面向SCR模型的系統(tǒng)安全性驗(yàn)證框架進(jìn)行描述，并對(duì)框架中的重要過程進(jìn)行基本介紹.

nuXmv語言能夠描述抽象自動(dòng)機(jī)，滿足對(duì)系統(tǒng)模型的需求規(guī)約安全性驗(yàn)證，因此本文將SS模型轉(zhuǎn)換為XMV模型并進(jìn)行驗(yàn)證.

圖2 安全性驗(yàn)證框架Fig.2 Security verification framework

驗(yàn)證框架如圖2所示，其中包括3個(gè)重要流程及其關(guān)鍵技術(shù)：

1)應(yīng)用ANTLR4[18]語法解析工具對(duì)輸入的SS模型語法分析獲取復(fù)雜單元和原子單元；

2)將復(fù)雜單元的變量約束平展化為底層的原子單元約束；

3)根據(jù)模型轉(zhuǎn)換規(guī)則將由原子單元約束構(gòu)建的SS模型轉(zhuǎn)換為XMV模型文件，進(jìn)行安全屬性驗(yàn)證.

本文整理了T-VEC語言的詞法和語法結(jié)構(gòu)，詞法規(guī)則采用正則表達(dá)式描述，語法結(jié)構(gòu)精確定義為擴(kuò)展巴克斯-諾爾范式[19](E-BNF)消除左遞歸.借助ANTLR4，本文對(duì)輸入的詞法文件的字符流進(jìn)行讀取，將字符聚類為單詞和符號(hào)(Token)；解析語法文件和識(shí)別語法結(jié)構(gòu)，最終生成每一個(gè)輸入的T-VEC語言模型的語法分析樹，并構(gòu)造語法結(jié)點(diǎn)遍歷器.ANTLR4語法程序parser根據(jù)T-VEC語法文件(grammer.g4)構(gòu)造生成語法分析樹，語法樹自上而下遞歸解析.其根結(jié)點(diǎn)是序列化語句的起始，包含了語法文件中描述的所有情況的文件結(jié)構(gòu)；其子結(jié)點(diǎn)是組成該文件結(jié)構(gòu)的所有遞歸詞組名；最下層的葉子結(jié)點(diǎn)即為實(shí)例中對(duì)應(yīng)該詞組名的具體單詞，整理出復(fù)雜單元和原子單元.

4 變量關(guān)系平展簡(jiǎn)化

4.1 平展簡(jiǎn)化算法

SS模型的遞歸定義體現(xiàn)在：在定義中間和輸出變量時(shí)，變量約束可以引入輸入變量、中間變量和輸出變量三類相關(guān)約束.其中，帶有中間變量和輸出變量的約束包含遞歸調(diào)用，存在更底層的變量約束，不具有原子性.變量約束的遞歸定義邏輯如圖3所示.

圖3 變量遞歸定義邏輯Fig.3 Form of recursive variables

因?yàn)镾S模型變量約束間存在遞歸嵌套，將每個(gè)包含約束定義的變量向上抽象為模型基本單元，其中：

1)ITO單元：帶有輸入、中間和輸出約束的可解釋變量單元；

2)IT單元：帶有輸入和中間約束的可解釋變量單元；

3)IO單元：帶有輸入和輸出約束的可解釋變量單元；

4)TO單元：帶有中間和輸出約束的可解釋變量單元；

5)T單元：僅帶有中間約束的基礎(chǔ)單元；

6)O單元：僅帶有輸出約束的基礎(chǔ)單元；

7)I單元：僅帶有輸入約束的基礎(chǔ)單元.

由圖3可知，每一個(gè)模型單元都可以向下解釋為包含同類單元約束的基本單元，即變量定義具有遞歸性；除基礎(chǔ)單元(I、T、O)外，每一個(gè)模型單元都可以解釋為下層基礎(chǔ)單元，即變量定義具有嵌套性；帶有同一種約束的基礎(chǔ)單元最終都可以簡(jiǎn)化為僅帶有輸入約束的I單元，即變量定義具有分解性.I單元是最底層的基礎(chǔ)單元，無法繼續(xù)向下解釋或化簡(jiǎn)，是整個(gè)系統(tǒng)的原子單元，沒有遞歸性、嵌套性和分解性.

本文利用模型單元的可分解性，將可解釋、可簡(jiǎn)化的變量單元向下層平展化簡(jiǎn)至原子單元I變量，打破SS模型遞歸、迭代和調(diào)用的特性，將復(fù)雜變量間的約束整理為上層單元與原子單元間的關(guān)系，滿足XMV模型線性、非調(diào)用的要求，完成模型轉(zhuǎn)換前的預(yù)操作.

本文提出的變量關(guān)系平展簡(jiǎn)化方式如圖4所示，對(duì)每個(gè)表述變量約束的樹形模型單元向下層平展，遍歷這個(gè)復(fù)雜模型單元的每一個(gè)分支，對(duì)每一個(gè)分支進(jìn)行深度檢索，直至將該單元以及該單元下層的復(fù)雜單元分解成基礎(chǔ)單元(I、T、O)，再將T和O單元簡(jiǎn)化為一組I單元.至此，將一個(gè)復(fù)雜單元向下平展簡(jiǎn)化為一個(gè)I基礎(chǔ)單元組，即從SS模型上說，將一個(gè)含有遞歸、嵌套的復(fù)雜變量約束關(guān)系轉(zhuǎn)換為一個(gè)僅含有輸入變量的約束關(guān)系組.

這種變量關(guān)系平展簡(jiǎn)化方式將樹形的SS模型變量約束定義轉(zhuǎn)換為XMV模型可接受的線性約束組，簡(jiǎn)化了模型轉(zhuǎn)換難度，達(dá)到了模型約束關(guān)系轉(zhuǎn)換的一致性，一定程度上減少模型狀態(tài)，使模型更加簡(jiǎn)潔.

圖4 模型單元平展簡(jiǎn)化過程Fig.4 Process of flattening model unit

變量約束平展簡(jiǎn)化算法如算法1所示.OutputVarConstr-aint(第1行)、termVarConstraint(第2行)和inputVarConstraint(第3行)分別代表輸入文件一個(gè)復(fù)雜單元中的輸出變量約束(O基礎(chǔ)單元)集合、中間變量約束(T基礎(chǔ)單元)集合和輸入變量約束(I原子單元)集合.平展時(shí)，首先針對(duì)輸出變量約束集合中的每一個(gè)O單元，判斷這個(gè)O單元是否為復(fù)雜單元，即存在其他的T、O單元(第5行)，如果存在，則向下遞歸，對(duì)這個(gè)O單元平展化，深度遍歷出O單元這個(gè)分支上的所有I單元并加入inputVarConstraint集合(第6行)，隨后將這個(gè)O單元的約束信息寫入預(yù)先設(shè)計(jì)好的termxml文件中(第7行)；如果不存在，則將這個(gè)O單元包含的原子約束加入inputVarConstraint集合，作為遞歸出口(第9行).然后，針對(duì)中間變量約束集合中的每一個(gè)T單元，做相應(yīng)操作，將每一個(gè)T單元平展簡(jiǎn)化為原子約束，加入原子約束集合，并將T單元的約束信息寫入到一個(gè)termxml文件中.最后，將描述所有原子約束的inputVarConstraint集合寫入到Modelname.pSS，完成平展簡(jiǎn)化后的文件輸出.

算法1.變量約束平展簡(jiǎn)化算法variableFlat

輸入：name.SS

輸出：Modelname.pSS，variablename.termxml

1.outputVarConstraint ← getOutput(name.SS)

2.termVarConstraint ← getTerm(name.SS)

3.inputVarConstraint ← getInput(name.SS)

4.Foreacho∈outputVarConstraintdo

5.IfexistTOunit(o)then

6.inputVarConstraint ← variableFlat(o)∪ inputVarConstraint

7.Writefile(variablename.termxml，o)

8.Else

9.inputVarConstraint ← inputVarConstraint ∪ getInput(o)

10.End

11.Foreacht∈termVarConstraintdo

12.IfexistTOunit(t)then

13.inputVarConstraint ← variableFlat(t)∪ inputVarConstraint

14.Writefile(variablename.termxml，t)

15.Else

16.inputVarConstraint ← inputVarConstraint ∪ getInput(t)

17.End

18.Writefile(name.pSS，inputVarConstraint)

19.Return Modelname.pSS，variablename.termxml

4.2 平展簡(jiǎn)化的意義與問題

變量約束關(guān)系的平展簡(jiǎn)化將樹形的約束邏輯平展為線性的約束邏輯，簡(jiǎn)化了后續(xù)的模型轉(zhuǎn)換過程.平展后的約束消除了嵌套性，成為同構(gòu)的線性約束，只需要制定好轉(zhuǎn)換規(guī)則就能夠?qū)ν瑯?gòu)的線性約束進(jìn)行批量操作.平展為線性的約束消除了遞歸性，直接構(gòu)建輸出變量與原子輸入變量的約束，取消了中間繁雜的、遞歸的約束轉(zhuǎn)換，減少了后續(xù)轉(zhuǎn)換的遍歷步驟，提高了運(yùn)行效率.平展操作讓輸出變量關(guān)于其他復(fù)雜變量的粗粒度約束簡(jiǎn)化為輸出變量關(guān)于原子變量的細(xì)粒度約束，有利于發(fā)現(xiàn)原本約束中重疊的部分，消除重復(fù)約束，優(yōu)化模型.

由于直接構(gòu)建頂層約束與底層約束的關(guān)聯(lián)，經(jīng)過平展簡(jiǎn)化后的變量約束會(huì)丟失中間過程和直接約束的信息，這不利于做完模型驗(yàn)證后追溯過程，找出存在問題的約束.這是平展簡(jiǎn)化存在的問題，省略了繁雜的中間信息，從而簡(jiǎn)化了模型轉(zhuǎn)換的過程.

針對(duì)這個(gè)問題，本文提出一種存儲(chǔ)中間信息的termxml格式.termxml文件基于xml格式，包含這個(gè)復(fù)雜單元下層的變量定義和對(duì)應(yīng)的相關(guān)約束.每一個(gè)復(fù)雜單元就存在一個(gè)對(duì)應(yīng)的中間信息文件.在對(duì)變量約束關(guān)系的平展簡(jiǎn)化中，算法同時(shí)對(duì)每一個(gè)復(fù)雜單元進(jìn)行了描述，將該單元包含的直接變量和相關(guān)約束封裝成預(yù)定好的規(guī)范化termxml格式文件，并進(jìn)行單獨(dú)文件輸出.

5 模型轉(zhuǎn)換規(guī)則定義

上一節(jié)主要介紹了變量關(guān)系平展簡(jiǎn)化，包括算法和平展簡(jiǎn)化的意義與問題.本節(jié)將在平展簡(jiǎn)化后的文件基礎(chǔ)上，對(duì)模型轉(zhuǎn)換過程中SS模型到XMV模型的規(guī)則定義與對(duì)應(yīng)的算法設(shè)計(jì)進(jìn)行詳細(xì)地闡述.

5.1 運(yùn)算符號(hào)轉(zhuǎn)換

SS模型支持算術(shù)運(yùn)算和邏輯運(yùn)算，算術(shù)運(yùn)算符包括四則運(yùn)算、絕對(duì)值、最大值、最小值和三角函數(shù)等常見的基本運(yùn)算符；邏輯運(yùn)算符包括邏輯與或非等推演布爾運(yùn)算符.XMV模型同樣支持同種類型的算術(shù)運(yùn)算和邏輯運(yùn)算，只是兩者所使用的符號(hào)不全一致，表1提供了運(yùn)算符對(duì)照表，在模型轉(zhuǎn)換過程中，每一個(gè)運(yùn)算符按表中規(guī)則轉(zhuǎn)換.

表1 運(yùn)算符對(duì)照表Table 1 Operator comparison table

5.2 類型轉(zhuǎn)換

SS模型支持基本類型的定義和基于基本類型的自定義類型定義，基本類型包括布爾型(Boolean)、整型(Integer)、浮點(diǎn)型(Float)和字符串型(String).自定義類型主要有兩類，分別是字符型的自定義類型和數(shù)值型的自定義類型：字符型自定義類型基于枚舉型(Enumerated)，可以擁有多個(gè)字符值；數(shù)值型自定義類型基于整型或浮點(diǎn)型，精確限制取值范圍，賦予類型現(xiàn)實(shí)意義.

表2 類型轉(zhuǎn)換對(duì)照表Table 2 Type conversion comparison table

XMV模型不支持字符串型和數(shù)值自定義類型的定義，因此用單例枚舉型作為字符串型的對(duì)照結(jié)果，用向上回溯的浮點(diǎn)型和整型作為數(shù)值自定義類型的對(duì)照結(jié)果.因?yàn)樵碱愋偷娜≈捣秶笥谧远x類型，所以并不影響類型轉(zhuǎn)換的一致性.精確定義：TBasic表示基本類型，TCustom表示自定義類型，TXMV表示XMV模型中的類型，則類型轉(zhuǎn)換規(guī)則表示為TBasic∪TCustom?TXMV，類型轉(zhuǎn)換對(duì)照表如表2所示.

5.3 常量轉(zhuǎn)換

5.4 變量轉(zhuǎn)換

在上一節(jié)的平展簡(jiǎn)化的介紹中，將SS模型引入的變量分為兩類：一類是不參與狀態(tài)遷移的輸入變量，對(duì)應(yīng)于SCR方法中的監(jiān)控變量，即原子單元(I)；另一類是通過狀態(tài)遷移描述系統(tǒng)運(yùn)行的中間變量和輸出變量，即復(fù)雜單元(T/O).XMV模型支持只參與初始賦值的輸入變量和貫穿整個(gè)系統(tǒng)的系統(tǒng)變量的定義，因此在變量轉(zhuǎn)換算法中，將原子單元的定義轉(zhuǎn)換為輸入變量定義，將復(fù)雜單元裝換為系統(tǒng)變量定義.SS模型中的變量在BNF中定義為VARIABLE ISA ，其中name代表變量名稱，type代表變量的類型.在XMV模型中，用IVAR關(guān)鍵字描述輸入變量，用VAR關(guān)鍵字描述系統(tǒng)變量，在BNF定義為IVAR/VAR identifiername：vartype，ASSIGN init(identifiername)：=value.精確定義：I和TO分別表示SS模型中的原子單元與復(fù)雜單元，IVAR和VAR分別表示XMV模型中的輸入變量和狀態(tài)變量，則有變量轉(zhuǎn)換規(guī)則為：SSI?XMVIVAR&SST0?XMVVAR.

變量聲明轉(zhuǎn)換算法如算法2所示.其中，Var是SS模型平展化后的系統(tǒng)存在變量集合.平展后SS模型描述了復(fù)雜單元與原子單元一對(duì)多的約束關(guān)系，因此在Var集合中包含O單元與I單元.變量定義轉(zhuǎn)換時(shí)，遍歷Var集合中的每一個(gè)單元，判斷其是否是原子單元(第3行)，如果是則將其轉(zhuǎn)換為輸入變量定義，如果不是則將其轉(zhuǎn)換為狀態(tài)變量定義(第6行).最后將轉(zhuǎn)換好的變量定義寫入到輸出文件中.

算法2.變量轉(zhuǎn)換算法

輸入：Modelname.pSS

輸出：Modelname.xmv

1.Var ← getModelVar(Modelname.pSS)

2.Foreachv ∈ Vardo

3.IfisIvar(v)then

4.ivar ← transform(v)

5.Else

6.var ← transform(v)

7.End

8.Writefile(Modelname.xmv，ivar)

9.Writefile(Modelname.xmv，var)

10.ReturnModelname.xmv

5.5 約束轉(zhuǎn)換

變量間的約束關(guān)系構(gòu)成了系統(tǒng)狀態(tài)的遷移，SS模型中的約束在邏輯結(jié)構(gòu)中指定，是基于謂詞的表達(dá)式.在平展簡(jiǎn)化后，一個(gè)邏輯結(jié)構(gòu)由一個(gè)或多個(gè)從屬原子約束連接組合.在XMV模型中，使用DEFINE關(guān)鍵字對(duì)每一條約束宏定義，定義為多條邏輯表達(dá)式，用邏輯符號(hào)連接.精確定義：LS代表SS模型中的邏輯結(jié)構(gòu)集合，C代表XMV模型中的約束集合，則約束轉(zhuǎn)換規(guī)則為：SSLSi?XMVCi，其中i=1，2…n.如圖5所示.

圖5 約束轉(zhuǎn)換規(guī)則Fig.5 Constraint transformation rules

約束轉(zhuǎn)換算法如算法3所示.其中l(wèi)ogicS代表平展后文件中所有邏輯結(jié)構(gòu)的集合，constraint用于存儲(chǔ)轉(zhuǎn)換后XMV模型中約束的集合，初始為空.在約束轉(zhuǎn)換時(shí)，遍歷logicS集合中每一個(gè)邏輯結(jié)構(gòu)l，采用字符替代方法將邏輯關(guān)系符號(hào)NOT、AND和OR分別轉(zhuǎn)換為對(duì)應(yīng)的符號(hào)，然后將每一個(gè)l轉(zhuǎn)換為一個(gè)宏定義的約束加入到constraint集合中，最后將集合寫入到文件中.

算法3.約束轉(zhuǎn)換算法

輸入：Modelname.pSS

輸出：Modelname.xmv

1.logicS ← getModelLogicS(Modelname.pSS)

2.constraint ← ?

3.Foreachl∈logicSdo

4.If“NOT：”inlthen

5.Replace(“NOT：”，!)

6.If“AND”inlthen

7.Replace(“AND”，“&”)

8.If“OR”inlthen

9.Replace(“OR”，“|”)

10.con ← transform(l)

11.constraint ← constraint ∪ con

12.End

13.Writefile(Modelname.xmv，constraint)

14.ReturnModelname.xmv

5.6 輸出賦值轉(zhuǎn)換

在SS模型中，輸出賦值表現(xiàn)了O單元在特定邏輯結(jié)構(gòu)下的特定取值；在XMV模型中，關(guān)鍵字next表現(xiàn)了狀態(tài)變量在特定條件下遷移到下一狀態(tài)的活動(dòng)；針對(duì)轉(zhuǎn)換好的約束宏定義，關(guān)鍵字case描述在當(dāng)前約束下狀態(tài)變量的下一狀態(tài)值.精確定義：f(ρ)=value代表SS模型中輸出賦值函數(shù)，其中ρ代表邏輯結(jié)構(gòu)，value代表變量值；next代表XMV模型狀態(tài)遷移的賦值過程，則輸出賦值的轉(zhuǎn)換規(guī)則為SSf?XMVnext，如圖6所示.

圖6 輸出賦值轉(zhuǎn)換規(guī)則Fig.6 Assignment conversion rules

輸出賦值算法如算法4所示.其中outputVariable代表輸出變量集合(第1行)，聲明一個(gè)assignmMap，key是已經(jīng)轉(zhuǎn)換好的約束的名稱，value是該變量在這個(gè)約束下的值.outAssignment代表轉(zhuǎn)換輸出賦值集合，其初值為空.在輸出賦值轉(zhuǎn)換過程中，遍歷每一個(gè)輸出變量，將其約束名稱和值按對(duì)應(yīng)的規(guī)則轉(zhuǎn)換，并加入輸出賦值集合，最后寫入到對(duì)應(yīng)文件中.

算法4.輸出賦值轉(zhuǎn)換

輸入：Modelname.pSS

輸出：Modelname.xmv

1.outputVariable ← getOutput(Modelname.pSS)

2.Statement assignmMap(constraintName，value)

3.outAssignment ← ?

4.Foreachvout ∈ outputVariabledo

5.assignmMap ← getMap(Modelname.pSS)

6.assign ← transform(vout，assignmMap)

7.outAssignment ← outAssignment ∪ assign

8.End

9.Writefile(Modelname.xmv，outAssignment)

10.ReturnModelname.xmv

5.7 轉(zhuǎn)換正確性證明

本章的前6節(jié)給出了SS模型到XMV模型的五條轉(zhuǎn)換規(guī)則，記作雙射函數(shù)φ(x).本節(jié)將給出相關(guān)邏輯證明，驗(yàn)證轉(zhuǎn)換規(guī)則的正確性.要證明轉(zhuǎn)換規(guī)則正確，需要對(duì)轉(zhuǎn)換前后的模型語義進(jìn)行分析，若語義不變，則轉(zhuǎn)換正確，否則判定轉(zhuǎn)換規(guī)則有錯(cuò)誤.為了判定模型語義，本文給出如下方法：如果轉(zhuǎn)換前后的SS模型和XMV模型都可以精確地描述同一個(gè)系統(tǒng)，則判定語義保持不變.本文使用有限狀態(tài)機(jī)(Finite State Machine)描述系統(tǒng)，首先給出有限狀態(tài)機(jī)的形式化語義描述.

定義3.一個(gè)有限狀態(tài)機(jī)(FSM)是一個(gè)五元組M=，其中：

1)Q是一個(gè)有窮狀態(tài)的集合；

2)Σ是輸入字母表，狀態(tài)機(jī)接收不同字母進(jìn)入不同狀態(tài)；

3)δ是狀態(tài)轉(zhuǎn)移函數(shù)δ×Σ→Q(擴(kuò)展函數(shù)δ×Σ*→Q)；

4)q0是初始狀態(tài)，q0∈Q；

5)F是終結(jié)狀態(tài)，F(xiàn)∈Q.

假設(shè)存在一個(gè)系統(tǒng)，其運(yùn)行狀態(tài)用有限狀態(tài)機(jī)M′描述為，這個(gè)狀態(tài)機(jī)有如下精確定義：

1)有窮集合Q′=.q0′表示系統(tǒng)初始狀態(tài)，qi′表示系統(tǒng)的中間狀態(tài)，F(xiàn)′表示系統(tǒng)終結(jié)狀態(tài)，其中i=1，2，…，n.

3)對(duì)于狀態(tài)中的每一組變量，不妨設(shè)變量類型type=，其中s≤t.

4)輸入字母表Σ′=<σ1，σ2，…，σm>.

5)狀態(tài)轉(zhuǎn)移函數(shù)δ′=<δ1，δ2，…，δk>，δi=qa′×σb→qc′，其中i≤k，a≤n，b≤n，c≤m.

6)q0′為初始狀態(tài)，q0′∈Q′.

7)F′為終結(jié)狀態(tài)，F(xiàn)′∈Q′.

針對(duì)這個(gè)精確定義的系統(tǒng)，采用2.2節(jié)介紹的SS模型，對(duì)它進(jìn)行形式化建模，系統(tǒng)模型SS′=，假設(shè)系統(tǒng)模型中前α類型不變，s-α類型可以縮小范圍重新自定義；不妨設(shè)輸入變量為1～r的變量，中間變量為r～θ的變量，輸出變量為θ～t變量；SS模型中的約束劃分為條件約束和事件約束，約束劃分為邏輯結(jié)構(gòu)和賦值函數(shù)，賦值函數(shù)為系統(tǒng)轉(zhuǎn)移函數(shù)，條件邏輯結(jié)構(gòu)為輸入字母表，事件邏輯結(jié)構(gòu)為輸入字母表與前一狀態(tài)轉(zhuǎn)移函數(shù)集合，其中元素對(duì)應(yīng)具體如下：

TBasic=；

TCustom=；

T=TBasic∪TCustom=；

Vin=；

Vterm=；

Vout=；

V=Vin∪Vterm∪Vout=；

SSLS=Σ′=<σ1，σ2，…，σm>；

SSLS′={Σ′，δn-1}；

SSf=δ′=<δ1，δ2，…，δk>；

Ccon=SSLS∪SSf；

Cet=SSLS′∪SSf；

C=Ccon∪Cet.

根據(jù)轉(zhuǎn)換雙射函數(shù)φ(x)可知，針對(duì)每一個(gè)SS模型，都有唯一的XMV=φ(SS)與之一一對(duì)應(yīng)；相反，針對(duì)每個(gè)XMV模型，都有唯一的SS=φ-1(XMV)與之一一對(duì)應(yīng).對(duì)于給定系統(tǒng)的SS′模型，若其轉(zhuǎn)換后的模型XMV′=φ(SS′)=<φ(T)，φ(V)，φ(T)>依然可以精確描述該系統(tǒng)，滿足系統(tǒng)狀態(tài)不變，則轉(zhuǎn)換前后語義不變，轉(zhuǎn)換規(guī)則正確，具體的轉(zhuǎn)換過程如下：

首先對(duì)系統(tǒng)模型變量關(guān)系平展簡(jiǎn)化，消除模型約束中的遞歸性和嵌套性，將整個(gè)系統(tǒng)模型定義為一個(gè)主模塊Mmain，根據(jù)TBasic∪TCustom?TXMV規(guī)則，將范圍擴(kuò)展成基礎(chǔ)類型，得到φ(T)=；根據(jù)SSI?XMVIVAR&SST0?XMVVAR規(guī)則，VAR=φ(V)=Vterm∪Vout=，IVAR=φ(V)=，其中變量類型為φ(T)集合元素，變量滿足性質(zhì)IVAR∩VAR=?；根據(jù)SSLS?XMVC規(guī)則，C=φ(C)=SSLS=<σ1，σ2，…，σm>；根據(jù)SSf?XMVnext規(guī)則，T=φ(C)=SSf=<δ1，δ2，…，δk>，其中變量與變量值組成的狀態(tài)集為S=，初始狀態(tài)S0=q0′，終結(jié)狀態(tài)F=F′，轉(zhuǎn)換后得到XMV′=，其中：

M=Mmain；

S=；

S0=q0′；

V=∪；

C=<σ1，σ2，…，σm>；

T=<δ1，δ2，…，δk>；

F=F′.

現(xiàn)在需要證明模型XMV′描述的系統(tǒng)為M′定義的系統(tǒng)，由于XMV是類自動(dòng)機(jī)模型，證明XMV′與M′模型等價(jià)，即證明其對(duì)應(yīng)系統(tǒng)元素?cái)?shù)值等價(jià)，非對(duì)應(yīng)系統(tǒng)元素語義等價(jià)即可.

對(duì)應(yīng)系統(tǒng)元素包括系統(tǒng)狀態(tài)集合、初態(tài)、終態(tài)和轉(zhuǎn)移函數(shù)集合.狀態(tài)集合S=Q′=，初態(tài)S0=q0′，終態(tài)F=F′，轉(zhuǎn)移函數(shù)集合T=δ′=<δ1，δ2，…，δk>，因此對(duì)應(yīng)系統(tǒng)元素?cái)?shù)值均對(duì)應(yīng)等價(jià).

非對(duì)應(yīng)系統(tǒng)元素包括模塊、變量集合和約束集合.其中，變量集合V與系統(tǒng)狀態(tài)包含的變量組一一對(duì)應(yīng)，變量類型也一致，達(dá)成語義等價(jià)；XMV′中的約束集合為引導(dǎo)狀態(tài)轉(zhuǎn)移的條件組，與M′系統(tǒng)中的字母表語義一致，且條件組均為<σ1，σ2，…，σm>；XMV′中的模塊為單個(gè)主模塊，是對(duì)整個(gè)系統(tǒng)的定義，沒有對(duì)系統(tǒng)元素精確定義，因此非對(duì)應(yīng)系統(tǒng)元素語義等價(jià).

在上述證明中可知，XMV′模型滿足M′系統(tǒng)的全部性質(zhì)和屬性，因此從語義上說，轉(zhuǎn)換前的SS′模型和轉(zhuǎn)換后的XMV′模型描述的是同一個(gè)系統(tǒng)M′，即可以判定轉(zhuǎn)換前后語義沒有發(fā)生改變，改變的只是模型的呈現(xiàn)形式，轉(zhuǎn)換雙射函數(shù)φ(x)包含的轉(zhuǎn)換規(guī)則是準(zhǔn)確的.

6 實(shí)例分析

6.1 系統(tǒng)描述

本章對(duì)航電系統(tǒng)中的飛行引導(dǎo)系統(tǒng)[20](Flight Guidance System，F(xiàn)GS)的控制單元進(jìn)行nuXmv安全性驗(yàn)證.首先根據(jù)該系統(tǒng)的需求描述建立SS變量關(guān)系模型，根據(jù)模型轉(zhuǎn)換規(guī)則φ(x)轉(zhuǎn)換為XMV模型，定義待驗(yàn)證屬性時(shí)序邏輯規(guī)約，最后一起作為模型檢測(cè)工具的輸入，進(jìn)行需求驗(yàn)證，分析驗(yàn)證結(jié)果.

飛行引導(dǎo)系統(tǒng)(FGS)是自動(dòng)飛行控制系統(tǒng)(Automatic Flight Control System，AFCS)的重要組成部分，F(xiàn)GS提供了飛行指引功能，接收大氣數(shù)據(jù)系統(tǒng)、姿態(tài)量測(cè)系統(tǒng)、導(dǎo)航系統(tǒng)等終端信息，根據(jù)FGS的模式邏輯和飛行控制律，后臺(tái)計(jì)算獲取操作指令，給出響應(yīng)，引導(dǎo)選擇正確的飛行模式，并監(jiān)督自動(dòng)駕駛儀和飛行指引儀的工作情況.

飛行控制律監(jiān)測(cè)飛行狀態(tài)，比較當(dāng)前飛機(jī)高度、姿態(tài)和速度等與模式期望值的差異，產(chǎn)生控制飛機(jī)趨近需求模式的飛行狀態(tài)引導(dǎo)指令.模式邏輯是選擇飛行模式的離散算法，描述了系統(tǒng)模式選擇和狀態(tài)激活的行為.本文將FGS中的模式邏輯作為研究對(duì)象，建立SS模型.

飛行模式可以分為橫向模式、垂直模式和偏航模式3個(gè)部分，橫向模式沿飛機(jī)軸線調(diào)整側(cè)滾角度控制水平運(yùn)動(dòng)，垂直模式沿機(jī)翼軸線調(diào)整俯仰角度控制豎直運(yùn)動(dòng)，偏航模式沿第三軸線控制飛行旋轉(zhuǎn).本節(jié)主要構(gòu)建前兩種模式下的簡(jiǎn)單飛行狀態(tài)的需求模型，其中橫向模式僅包含側(cè)滾模式ROLL和航向選擇模式HDG，垂直模式僅包含俯仰模式PITCH和垂直速度模式VS.傳統(tǒng)的建模分析方法如：Markov Process[21]和故障樹分析[22]等與系統(tǒng)規(guī)約形式之間有很大的不同，無法直接應(yīng)用.而XMV模型不能直接接受包含多種模式轉(zhuǎn)換和數(shù)值計(jì)算的FGS模型給出的自然語言需求的輸入，也無法將這些需求轉(zhuǎn)換為XMV可接受的類狀態(tài)機(jī)模型.另一方面，基于表格表達(dá)式的SS模型對(duì)需求關(guān)系的描述能力很強(qiáng)，對(duì)于規(guī)范好的FGS系統(tǒng)需求可以實(shí)現(xiàn)模型的自動(dòng)建立，但是缺乏自我驗(yàn)證的能力，本文給出的方法同時(shí)具備上述兩種模型的優(yōu)點(diǎn)，對(duì)FGS系統(tǒng)變量提取建立模型，通過模型轉(zhuǎn)換算法得到XMV模型，然后進(jìn)行屬性驗(yàn)證.

6.2 變量提取

首先對(duì)系統(tǒng)中所需要的變量進(jìn)行類型定義，除了基本的變量類型之外，F(xiàn)GS系統(tǒng)的自定義類型有表示指示燈亮滅的yLamp，其原始類型為枚舉，枚舉值有off(燈滅)和on(燈亮)，默認(rèn)初始值為off；表示飛機(jī)超速提示的yOverspeed，其原始類型為枚舉類型，枚舉值有undefined(未知)、yes(超速)和no(未超速)，默認(rèn)初始值為undefined；表示開關(guān)的ySwitch，原始類型為枚舉類型，枚舉值為off(關(guān))和on(開)，默認(rèn)初始值為off.

根據(jù)FGS的簡(jiǎn)單層次架構(gòu)，F(xiàn)GS系統(tǒng)引入的數(shù)據(jù)有飛機(jī)超速提示Overspeed、自動(dòng)駕駛儀接通提示AP_Engage_Switch、飛機(jī)控制面板控制提示FD_Switch、同步開關(guān)SYNC_Switch、航向選擇開關(guān)HDG_Switch和垂直速度開關(guān)VS_Switch，將其作為系統(tǒng)輸入變量，如表3所示.

表3 輸入變量Table 3 Input variables

在FGS簡(jiǎn)單層次模型中，有AP、FD、HDG、VS、ROLL和PITCH系統(tǒng)狀態(tài)機(jī)，各子系統(tǒng)間系統(tǒng)內(nèi)互相獨(dú)立，系統(tǒng)外互相關(guān)聯(lián)，本文選取其中航向選擇模式(HDG)作為典型實(shí)例，闡述模式建模過程.

模式間存在復(fù)雜的優(yōu)先級(jí)關(guān)系，在HDG子系統(tǒng)中引入中間變量HDGNoHigher、HDGPressed、HDGSelect和HDGDeselect分別用于表示沒有優(yōu)先級(jí)更高的事件發(fā)生、HDG開關(guān)打開且被系統(tǒng)有效接收、選擇和取消HDG模式，如表4所示.

表4 中間變量Table 4 Intermediate variables

根據(jù)已經(jīng)定義好的中間變量，可以建立HDG模式表，用于表示飛機(jī)在航向選擇模式下的狀態(tài)切換，包括未知(undefined)、未選中(cleared)和被選中(selected)3個(gè)模式取值.表5是HDG模式遷移表，初始值為undefined.

表5 HDG模式類表Table 5 Migration table of HDG

FGS系統(tǒng)的輸出主要表現(xiàn)在飛行顯示面板上的模式提示指示燈，依賴于系統(tǒng)輸入在模式邏輯的控制下的狀態(tài)改變.如果指示燈亮，則對(duì)應(yīng)飛行模式激活；如果指示燈滅，則對(duì)應(yīng)的飛行模式未工作.每一個(gè)飛行模式和系統(tǒng)輸入對(duì)應(yīng)一個(gè)輸出變量，輸出變量如表6所示.

表6 輸出變量Table 6 Output variables

6.3 屬性驗(yàn)證

完成FGS的模型建立后，按照第4節(jié)的算法對(duì)模型進(jìn)行平展簡(jiǎn)化，將HDG模式包含的上層約束中的HDGNoHigher 、HDGPressed 和HDGSelect等TO單元向下簡(jiǎn)化為SYNC_Switch和HDG_Switch等I單元，消除變量間的間接約束，直接構(gòu)建HDG模式undefined、cleared和selected狀態(tài)與HDG模式開關(guān)的關(guān)系.

按照第5節(jié)中定義的轉(zhuǎn)換規(guī)則，將平展好的SS模型轉(zhuǎn)換為XMV模型，并解釋為nuXmv可輸入的smv文件.其中包括開關(guān)類型的轉(zhuǎn)換，根據(jù)變量轉(zhuǎn)換算法，將抽取出的關(guān)于控制開關(guān)信息的輸入變量轉(zhuǎn)換為IVAR，將關(guān)于模式優(yōu)先級(jí)信息的中間變量和關(guān)于信號(hào)燈信息的輸出變量轉(zhuǎn)換為VAR；根據(jù)約束轉(zhuǎn)換算法，將HDG模式類表和變量表中抽取出來的變量的條件和事件關(guān)系轉(zhuǎn)換為約束集合；根據(jù)輸出賦值轉(zhuǎn)換算法，將輸出變量表中提取的賦值關(guān)系，轉(zhuǎn)換為狀態(tài)遷移關(guān)系.

驗(yàn)證安全屬性是保證FGS系統(tǒng)安全性和正確性的重要方法，本文從FGS系統(tǒng)中抽取了系統(tǒng)需求規(guī)約，添加到smv描述文件中，對(duì)系統(tǒng)安全性進(jìn)行驗(yàn)證.

正例驗(yàn)證，本文選取HDG模式的狀態(tài)遷移規(guī)約.航向模式有undefined、cleared和selected這3個(gè)狀態(tài)，當(dāng)飛行模式打開，系統(tǒng)確認(rèn)HDG激活，則從cleared遷移至selected；當(dāng)飛行模式打開，系統(tǒng)確認(rèn)HDG取消，則從selected遷移至cleared.若規(guī)約安全，將返回True確認(rèn)該屬性安全，給出時(shí)序邏輯規(guī)約描述如下：HDG模式不可能一直處于激活狀態(tài)LTLSPEC !G(HDG=Selected)，具體正例驗(yàn)證如圖7所示.

圖7 實(shí)驗(yàn)結(jié)果圖Fig.7 Experimental results

反例驗(yàn)證，本文選取HDG模式的狀態(tài)遷移規(guī)約，注入錯(cuò)誤規(guī)約，HDG模式將一直處于激活狀態(tài)，這顯然是不正確的性質(zhì)規(guī)約.若規(guī)約不符合模型，將返回反例路徑，提示屬性不安全，給出時(shí)序邏輯規(guī)約描述如下：LTLSPEC G(HDG=Selected)，具體反例路徑如圖7所示.

7 相關(guān)工作與結(jié)束語

目前在安全關(guān)鍵領(lǐng)域，系統(tǒng)的安全性分析是提高機(jī)載系統(tǒng)軟件需求規(guī)約正確性和一致性的重要方法.很多工業(yè)界和學(xué)術(shù)界的研究者所做的相關(guān)工作可以分為兩類，其一是針對(duì)系統(tǒng)及軟件需求問題進(jìn)行建模分析工作：文獻(xiàn)[5]介紹了應(yīng)用于計(jì)算機(jī)系統(tǒng)的模型的安全評(píng)估方法及其對(duì)系統(tǒng)進(jìn)行安全性分析的工作；在基于模型的評(píng)估方法上，SCR模型是一種較為常用的建模方法，文獻(xiàn)[9]介紹了基于變量關(guān)系的SCR模型，并根據(jù)其建模方法對(duì)燈光控制系統(tǒng)進(jìn)行形式化建模工作；文獻(xiàn)[10]介紹了SCR方法解決了變量關(guān)系建模問題，提供了一套完整的系統(tǒng)形式化方法；其二是應(yīng)用形式化工具進(jìn)行分析與驗(yàn)證工作：文獻(xiàn)[11]介紹了演繹證明、模型驗(yàn)證和抽象解釋3種形式化驗(yàn)證的重要方法，并解釋了形式化驗(yàn)證的過程.文獻(xiàn)[14]和文獻(xiàn)[15]介紹了能夠描述抽象自動(dòng)機(jī)，基于狀態(tài)的自動(dòng)化驗(yàn)證工具nuXmv，實(shí)現(xiàn)了使用nuXmv模型工具進(jìn)行安全性評(píng)估和分析.

相較而言，當(dāng)前的建模分析工作缺少形式化工具的深度驗(yàn)證，在需求的完整性和一致性上要求不夠.對(duì)安全關(guān)鍵系統(tǒng)建模僅能描述系統(tǒng)的需求設(shè)計(jì)，而不能遍歷檢查系統(tǒng)的全部狀態(tài)，不足以滿足對(duì)于系統(tǒng)模型的精確分析和驗(yàn)證的要求.尤其是當(dāng)現(xiàn)代的機(jī)載系統(tǒng)功能越來越復(fù)雜，規(guī)模越來越龐大，對(duì)于大量的需求規(guī)約，停留在建模階段的形式化工作無法支撐其安全等級(jí)的任務(wù)要求.因此，用模型映射的方法，對(duì)SCR模型轉(zhuǎn)換，實(shí)現(xiàn)系統(tǒng)全部狀態(tài)的驗(yàn)證是本文的研究重點(diǎn).

針對(duì)機(jī)載系統(tǒng)的安全性分析問題，本文提出了一種采用模型映射的驗(yàn)證方法，設(shè)計(jì)了從描述變量關(guān)系的SS模型到模型檢測(cè)XMV模型的轉(zhuǎn)換工具，能夠自動(dòng)化地完成模型編輯、模型轉(zhuǎn)換的功能.在具體實(shí)現(xiàn)上，首先根據(jù)系統(tǒng)軟件的關(guān)系邏輯建立系統(tǒng)的SS模型，設(shè)計(jì)變量關(guān)系平展簡(jiǎn)化算法，消除變量間遞歸且嵌套的間接約束定義，獲得簡(jiǎn)單狀態(tài)模型.借助語法分析工具ANTLR4，建立輸入描述SS模型的語法文件的語法分析樹，定義模型語法映射規(guī)則，通過遍歷語法樹結(jié)點(diǎn)，實(shí)現(xiàn)轉(zhuǎn)換為XMV模型.最后，基于XMV模型使用模型檢驗(yàn)工具nuXmv對(duì)安全屬性規(guī)約驗(yàn)證，根據(jù)返回的結(jié)果找出系統(tǒng)設(shè)計(jì)的安全性問題，在系統(tǒng)失效前及時(shí)修改，保證關(guān)鍵系統(tǒng)的安全性.

未來的進(jìn)一步工作由以下兩方面構(gòu)成：

1)本文給出的模型映射規(guī)則在約束元素上還有改進(jìn)空間，將對(duì)時(shí)間[23]等復(fù)雜約束繼續(xù)進(jìn)行研究；

2)安全屬性的抽取仍需要人工解釋自然語言為標(biāo)準(zhǔn)規(guī)約語句，存在一定的局限性，之后將進(jìn)一步提高工具的自動(dòng)化程度，擴(kuò)展其適用范圍.