基于ANTLR的AltaRica 3.0模型平展化算法設(shè)計與實現(xiàn)

陳 朔，胡 軍，王立松

1(南京航空航天大學(xué) 計算機(jī)科學(xué)與技術(shù)學(xué)院，南京 211106) 2(軟件新技術(shù)與產(chǎn)業(yè)化協(xié)同創(chuàng)新中心，南京 210007)

1 引 言

目前隨著工業(yè)系統(tǒng)的規(guī)模不斷增加，系統(tǒng)故障往往會引起重大的生命和財產(chǎn)損失[1]，因此安全關(guān)鍵系統(tǒng)的安全性和可靠性分析就顯得尤為重要.但是傳統(tǒng)系統(tǒng)工程無法很好的解決復(fù)雜安全關(guān)鍵系統(tǒng)的模型構(gòu)建和分析問題[2]，基于MBSA(Model-Based safety assessment)的安全關(guān)鍵系統(tǒng)分析方法在近些年來逐步受到業(yè)界的廣泛關(guān)注[3].MBSA的核心是首先對整個系統(tǒng)進(jìn)行模型構(gòu)建，然后通過對整個模型的定性和定量分析，來發(fā)現(xiàn)模型中可能存在的安全缺陷和潛在的系統(tǒng)風(fēng)險.MBSA通過在系統(tǒng)模型設(shè)計層級進(jìn)行安全分析，消除這些風(fēng)險可能導(dǎo)致的后果，提高整個系統(tǒng)的安全性[4].

AltaRica 3.0[5-7]是一種基于MBSA的多層次的模型語言，并結(jié)合形式化方法對系統(tǒng)的安全性進(jìn)行分析，目前在航空航天系統(tǒng)安全分析領(lǐng)域有著較為廣泛的應(yīng)用.AltaRica 3.0模型中的層次結(jié)構(gòu)S2ML是用來描述真實系統(tǒng)的復(fù)雜層次架構(gòu)和相應(yīng)系統(tǒng)中部件的關(guān)聯(lián)信息，而要對AltaRica 3.0模型進(jìn)行安全性驗證，就要將AltaRica 3.0模型的層次結(jié)構(gòu)轉(zhuǎn)換成形式化語義模型，AltaRica 3.0的形式化語義模型是一類衛(wèi)士轉(zhuǎn)換系統(tǒng)GTS(Guarded Transition Systems)[8]，由于GTS所具有的的形式化語義特征，就可以應(yīng)用馬爾可夫生成器[9]、隨機(jī)仿真、模型檢測等工具進(jìn)行對AltaRica 3.0模型進(jìn)行有效的安全性分析與驗證.因此，將AltaRica 3.0的層次模型(S2ML)轉(zhuǎn)換為語義等價的平展化模型(GTS)是進(jìn)行系統(tǒng)安全分析的一個關(guān)鍵步驟.

本文的主要研究內(nèi)容如下：第2節(jié)介紹本文的相關(guān)工作和國內(nèi)外研究現(xiàn)狀；第3節(jié)討論了本文研究所涉及技術(shù)的基本概念和說明；第4節(jié)詳細(xì)描述了AltaRica 3.0的ANTLR解析過程，進(jìn)行AST驗證，并給出本文所設(shè)計的平展化算法的思想和偽代碼的描述，對算法進(jìn)行復(fù)雜度分析，以及對算法的優(yōu)化部分進(jìn)行了說明；最后在第5節(jié)中，進(jìn)行實驗的評估，并在第6節(jié)中總結(jié)和討論了未來的工作.

2 相關(guān)工作

目前，已經(jīng)發(fā)布了三個AltaRica版本：AltaRica 1.0[10]，AltaRica DataFlow[11，12]和AltaRica 3.0，其中第一版的AltaRica 1.0主要是根據(jù)約束自動機(jī)定義的[6]，針對第一版的AltaRica模型，已經(jīng)有幾種評估工具被開發(fā)，例如模型檢查器[13]和關(guān)鍵序列生成器[14].但是第一版的AltaRica模型在處理大型工業(yè)系統(tǒng)過程時，會消耗大量的資源.針對這個問題，第二版的AltaRica Data-Flow模型被創(chuàng)建，它的語義是基于模式自動機(jī)的[15].在這個版本中，斷言中只允許數(shù)據(jù)流的分配，AltaRica Data-Flow已經(jīng)在Cecilia OCAS，Simfia[16，17]和Safety Designer中得到廣泛的應(yīng)用.AltaRica 3.0是AltaRica的第三個版本，雖仍處于實驗室的研究階段，但相比于AltaRica Data-Flow，AltaRica 3.0增加了GTS和面向?qū)ο蟮母拍?，其中GTS是AltaRica 3.0的基礎(chǔ)數(shù)學(xué)模型，可以對AltaRica 3.0模型進(jìn)行安全性分析與驗證，對象的概念使AltaRica 3.0更符合編程語言的語法思想.

國內(nèi)對AltaRica 3.0的研究還是空白階段，在航空電子系統(tǒng)進(jìn)行安全驗證的時候，我們只能對已有的AltaRica工具(如Simfia等)進(jìn)行工具應(yīng)用，同時國外對AltaRica工具的進(jìn)行技術(shù)保密，無法掌握其核心技術(shù)和工作原理.因此了解AltaRica 3.0的平展化操作原理，實現(xiàn)AltaRica 3.0的GTS獲取過程，是下一步開發(fā)基于AltaRica 3.0的自主安全分析軟件的重要基礎(chǔ)，對航空系統(tǒng)安全性分析有重大意義.國外已有的工作包括：文獻(xiàn)[18]主要介紹AltaRica 1.0的平展化操作，文獻(xiàn)[19]中的平展化工作是針對AltaRica Data-Flow而言，不能對AltaRica 3.0模型進(jìn)行平展化操作，文獻(xiàn)[20]中的只介紹了AltaRica 3.0平展化的基本思想和要求，沒有進(jìn)行詳細(xì)的實現(xiàn)，目前沒有針對AltaRica 3.0的平展化算法的實際實現(xiàn).

為此，本文提出了一種基于ANTLR的AltaRica 3.0的平展化算法A2GTS，用來完成AltaRica 3.0的平展化操作，A2GTS利用ANTLR生成AltaRica 3.0的抽象語法樹AST(Abstract Syntax Tree)，然后使用樹的遍歷算法，可以快速準(zhǔn)確的定位到存儲信息的結(jié)點，從而獲取到結(jié)點的存儲信息，提高整個平展化系統(tǒng)的速度和精確度.

3 ANTLR與AltaRica 3.0概述

3.1 ANTLR概述

本文工作中涉及到模型語言的識別和轉(zhuǎn)換，因此采用ANTLR平臺來實施.ANTLR是一種基于EBNF的語法分析器工具，可用于讀取、處理、執(zhí)行和翻譯結(jié)構(gòu)化的文本或者二進(jìn)制的文件[21]，在學(xué)術(shù)領(lǐng)域和實際的工業(yè)生產(chǎn)中得到廣泛的應(yīng)用.在ANTLR中，首先需要將所分析語言的語法規(guī)則定義為ANTLR語法解析文件的格式(ANTLR的元語言(Meta Language)[22])，形成要解析語言的ANTLR語法文件；其次通過調(diào)用ANTLR的內(nèi)置方法，生成對應(yīng)的詞法分析器和語法分析器.

詞法分析器的功能是根據(jù)相應(yīng)的詞法規(guī)則將輸入文件的字符流轉(zhuǎn)換成由短語組成的標(biāo)記流，得到具體語言的詞法分析結(jié)果；然后利用語法分析器將這些標(biāo)記流進(jìn)行組合，生成一棵抽象語法樹AST.所有的詞法信息都是存儲在AST的葉子結(jié)點上，可以根據(jù)具體語言處理的不同要求來制定相應(yīng)的處理規(guī)則，獲取最終的執(zhí)行結(jié)果.

圖1 ANTLR解析過程

如圖1所示，ANTLR的主要解析過程分為詞法分析，語法分析，AST分析和相關(guān)模板文件分析四個過程[23]，具體過程如下：

1)詞法分析過程：高級語言以輸入文本的方式進(jìn)入到詞法解析器中，經(jīng)過詞法解析器的解析成為特定的標(biāo)記流(token)，緩存在內(nèi)存中.

2)語法分析過程：詞法分析器獲取的標(biāo)記流信息直接傳遞給語法分析器，根據(jù)語言的ANTLR解析文件，獲取詞法信息中包含的語法信息.

3)AST分析過程：生成抽象的語法樹，AST主要包含兩部分的內(nèi)容：結(jié)構(gòu)信息，包含整個輸入的語法實例的結(jié)構(gòu)信息；文本信息，詞法分析中得到的標(biāo)記流都存儲在AST的葉子結(jié)點中，可以使用ANTLR的監(jiān)聽器和訪問器方法對整棵樹進(jìn)行遍歷.

4)自定義轉(zhuǎn)換過程：通過制定的轉(zhuǎn)化規(guī)則，就可以對獲取的文本信息進(jìn)行相應(yīng)的轉(zhuǎn)換，產(chǎn)生特定的輸出文本，獲取到轉(zhuǎn)換后的文件.

3.2 AltaRica 3.0模型

AltaRica 3.0是基于事件的建模語言，主要由系統(tǒng)結(jié)構(gòu)建模語言S2ML和衛(wèi)士轉(zhuǎn)換系統(tǒng)GTS組成[20]，其中S2ML是描述AltaRica 3.0的層次結(jié)構(gòu)的模型語言，GTS則用來對AltaRica 3.0進(jìn)行安全分析的形式化語義模型.

AltaRica 3.0是層次化的語言，可以包含多個嵌套遞歸結(jié)構(gòu)，直接使用多層次化的AltaRica 3.0模型來對整個系統(tǒng)進(jìn)行安全性分析是非常復(fù)雜的.GTS模型本質(zhì)上是由一個基于自動機(jī)同步交互網(wǎng)絡(luò)的形式化模型，且目前已有較為成熟的基于自動機(jī)網(wǎng)絡(luò)模型的形式化分析技術(shù)(如：支持模型檢驗的軟件工具，NuSMV，SPIN等)，因此將多層次的AltaRica 3.0模型轉(zhuǎn)換成等價語義的平展化GTS模型，就可以很好的應(yīng)用模型檢驗工具來進(jìn)行有效嚴(yán)格的安全性分析.

AltaRica 語言有著嚴(yán)格的語法和詞法定義[19].模型的基本組件是結(jié)點(Class/Block).主要由變量(Variable，包括流變量和狀態(tài)變量)、事件(Event，事件發(fā)生后，會引起變量的轉(zhuǎn)換)、轉(zhuǎn)換(Transition，包括正常轉(zhuǎn)換，同步轉(zhuǎn)換和隱藏轉(zhuǎn)換，對系統(tǒng)的狀態(tài)變化進(jìn)行說明)、斷言(Assertion，描述流變量和狀態(tài)變量、流變量之間的關(guān)系)組成[21].為了詳細(xì)說明AltaRica 3.0的組成信息，圖2給出了一個冷卻系統(tǒng)的圖示及其AltaRica 3.0模型表述.

圖2

AltaRica 3.0利用面向?qū)ο蟮乃枷?，將圖2(a)的冷卻系統(tǒng)中的具體組件抽象成類.水箱、泵和反應(yīng)堆分別是Tank類、Pump類和Reactor類，類之間通過變量進(jìn)行交互，Tank類實例化對象T的冷卻液輸出作為整個系統(tǒng)的輸出變量outFlow，Pump類的兩個實例化對象P1和P2分別有兩個變量：輸入變量inFlow和輸出變量outFlow，Reactor的輸入變量inFlow和P1、P2的輸出變量outFlow相同.系統(tǒng)要保證至少有一個泵保持正常的運轉(zhuǎn)狀態(tài)，這樣冷卻液才能夠準(zhǔn)確地對反應(yīng)堆進(jìn)行冷卻操作，但是泵可能發(fā)生故障，水箱也可能為空，這些原因都能導(dǎo)致整個系統(tǒng)的失效.圖2(b)利用AltaRica 3.0對整個系統(tǒng)進(jìn)行描述，定義了上述系統(tǒng)的組件信息和可能發(fā)生的失效事件信息.

GTS是一類支持安全分析的狀態(tài)/轉(zhuǎn)換形式的模型，可以用來表示具有即時環(huán)路的系統(tǒng)，描述系統(tǒng)組件在環(huán)路中的狀態(tài)轉(zhuǎn)換.GTS對系統(tǒng)進(jìn)行描述的模型稱為平展化的模型，AltaRica 3.0多層次模型轉(zhuǎn)換為GTS模型的過程稱為平展化操作.圖2冷卻系統(tǒng)的GTS模型表述如下.

block CoolingSystem

Boolean T.isEmpty(init=false)；

Boolean T.outFlow(reset=false)；

RepairableState LineOne.POne.s，

LineTwo.PTwo.s(init=WORKING)；

Boolean LineOne.POne.inFlow，

LineOne.POne.outFlow(reset=false)；

Boolean LineTwo.PTwo.inFlow，

LineTwo.PTwo.outFlow(reset=false)；

Boolean Reactor.inFlow(reset=false)；

event T.getEmpty；

event LineOne.POne.failure，LineOne.POne.repair；

event LineTwo.PTwo.failure，LineTwo.PTwo.repair；

transition

T.getEmpty：not T.isEmpty-> T.isEmpty：=true；

LineOne.POne.failure：LineOne.POne.s==

WORKING-> LineOne.POne.s：=FAILED；

LineOne.POne.repair：LineOne.POne.s==

FAILED-> LineOne.POne.s：=WORKING；

LineTwo.PTwo.failure：LineTwo.PTwo.s==

WORKING-> LineTwo.PTwo.s：=FAILED；

LineTwo.PTwo.repair：LineTwo.PTwo.s==

FAILED-> LineTwo.PTwo.s：=WORKING；

assertion

T.outFlow：=if not T.isEmpty then true else false；

LineOne.POne.inFlow：=T.outFlow；

LineTwo.PTwo.inFlow：=T.outFlow；

LineOne.POne.outFlow：=if LineOne.POne.s==

WORKING then LineOne.POne.inFlow else false；

LineTwo.PTwo.outFlow：=if LineTwo.PTwo.s==

WORKING then LineTwo.PTwo.inFlow else false；

Reactor.inFlow：=LineOne.POne.outFlow or

LineTwo.PTwo.outFlow；

end

對AltaRica 3.0的多層次結(jié)構(gòu)模型S2ML進(jìn)行平展化處理，利用面向?qū)ο蟮乃枷?，將多個類編譯成一個GTS模型，其中變量、參數(shù)、觀察變量、事件按照調(diào)用關(guān)系重新命名，例如主類main中有一個對象a，a中有一個對象b，b中有一個變量s，那么s在GTS中可表示為a.b.s，例如Reactor中的inFlow變量在GTS中被表述為Reactor.inFlow，通過這種方式，AltaRica 3.0模型的層次結(jié)構(gòu)信息被完整表達(dá)，但是對應(yīng)的GTS模型只有一層結(jié)構(gòu)，從而簡化了整個模型的層次結(jié)構(gòu).

使用AltaRica 3.0模型描述的某復(fù)雜結(jié)構(gòu)的系統(tǒng)模型都可以轉(zhuǎn)換成等效的平展化GTS模型.本文根據(jù)AltaRica 3.0和GTS的語法規(guī)則，制定了相應(yīng)的轉(zhuǎn)換規(guī)則，設(shè)計了一套轉(zhuǎn)換算法A2GTS，實現(xiàn)AltaRica 3.0模型自動轉(zhuǎn)換成為對應(yīng)的GTS平展化模型.

4 基于ANTLR的AltaRica 3.0平展化算法框架

本節(jié)利用基于ANTLR的AltaRica 3.0語法解析文件和平展化操作的基本思想，提出了一種基于ANTLR的AltaRica 3.0模型平展化實現(xiàn)算法(A2GTS).首先介紹算法的基本思想，其次描述算法的基本步驟和偽代碼說明，最后對算法進(jìn)行復(fù)雜度和優(yōu)化分析.

4.1 形式化轉(zhuǎn)換過程

定義1.由AltaRica 3.0的S2ML模型轉(zhuǎn)換成為AltaRica 3.0的GTS模型的過程叫做AltaRica 3.0的平展化操作.

一個簡單的平展化過程如下所示.

block A中包含block B，平展化過程只保留一層結(jié)構(gòu)信息，因此對block B進(jìn)行平展化操作，同時也要保證模型結(jié)構(gòu)信息的完整表達(dá)，對于B中的組件信息用B.p的形式保留其模型結(jié)構(gòu)信息.由于S2ML和GTS的詞法信息相同，僅僅是語法結(jié)構(gòu)上的不同，因此對于兩個模型信息中的詞法信息可以直接對應(yīng)，僅需考慮語法結(jié)構(gòu)上的轉(zhuǎn)換.

定義2.衛(wèi)士轉(zhuǎn)換系統(tǒng)(GTS)是一個五元組[20]：

G=

(1)

?V是一組變量，分為狀態(tài)變量S和流變量F，S用來描述系統(tǒng)組件的狀態(tài)信息，F(xiàn)是系統(tǒng)組件之間的交互流變量，其中V=S∪F，并且S∩F=?；

?E是GTS中所有transition事件的集合，為系統(tǒng)可能發(fā)生的一組事件，主要由正常事件Enor和同步事件Esyn組成，即E=Enor∪Esyn；

?T是一組轉(zhuǎn)換(transition)，即三元組，也可表示為e：G→P，其中e是E的事件，G為狀態(tài)變量和流變量的布爾條件，構(gòu)建在集合V上的布爾公式，P是建立在變量上的指令，對狀態(tài)變量執(zhí)行的動作，用于計算系統(tǒng)的新狀態(tài)；

?A是斷言(assertion)，即建立在V變量上的指令，用于根據(jù)狀態(tài)變量的值計算流變量的值；

?ξ是V的變量分配，是對狀態(tài)變量和流變量的初始賦值，其中狀態(tài)變量的初始化的關(guān)鍵字為“init”，流變量的初始化的關(guān)鍵字為“reset”.

轉(zhuǎn)換e：G→P可以在給定的狀態(tài)ε下，流變量和狀態(tài)變量組合的布爾條件為真，G為真(即給定的流變量和狀態(tài)變量賦值集合為ε)：

ε(G)=TRUE

(2)

e：G→P的過程分為兩步：首先，G的布爾條件為真，此時就可以通過P更新系統(tǒng)組件的狀態(tài)變量；其次，斷言A就可以根據(jù)新的狀態(tài)變量的值，更新系統(tǒng)組件的流變量值.

定義3.系統(tǒng)結(jié)構(gòu)建模語言(S2ML)是一個四元組：

S=

(3)

?A(Attributes)代表變量的屬性信息，是一組變量的賦值，屬性用于將信息與端口，連接和塊相關(guān)聯(lián)，表示S2ML模型中組件狀態(tài)變量和流變量的屬性信息，可用于描述組件之間的交互，即：name=value(name為變量名稱，value為變量賦值)；

?P(Ports)代表系統(tǒng)中組件的抽象類信息，AltaRica 3.0利用面向?qū)ο蟮乃枷雽⒄鎸嵪到y(tǒng)中的組件進(jìn)行抽象，端口是模型的基本對象，包括variables，events和transitions，即：

P=Pv∪Pe∪Pt

(4)

?C(Connections)是描述Ports之間的交互信息，用來詳細(xì)說明模型中組件之間的流變量交互行為.

?B(Blocks)相當(dāng)于容器.包含了Ports，Connections和其他的Blocks，即：

B=BP∪BC∪Bsub

(5)

假設(shè)S1是一個真實的S2ML模型，其中S1=，G1是S1扁平化后的GTS模型，其中G1=.

第一，詞法層面轉(zhuǎn)換.S1中的變量的屬性信息A1對應(yīng)G1中的ξ1，即A1=ξ1；S1中的P1由變量信息、事件信息和轉(zhuǎn)換信息組成，即P1=Pv1∪Pe1∪Pt1，因此Pv1對應(yīng)G1中的V1，Pe1對應(yīng)G1中的E1，Pt1對應(yīng)G1中的T1，P1=Pv1∪Pe1∪Pt1可表述為P1=V1∪E1∪T1；S1中的C1描述P1中流變量的交互信息，因此C1=A1.

第二，語法層面轉(zhuǎn)換.假設(shè)S1中的B1包含n層子模塊Bsub1_j(0≤j≤n，0≤n≤+)，每層Bsub1_j包含m個Bsub1_ji(0≤i≤m，0≤m≤+)，即一個B1可由m×n個Bsub1組成，此時假設(shè)B1的模塊名稱為b1，Bsub1_j的模塊名稱為bsub1_j，Bsub1_ji的模塊名稱為bsub1_ji.則S2ML中的結(jié)構(gòu)層次關(guān)系在GTS中表述為b1.bsub1_j.bsub1_ji，GTS由“.”來表達(dá)模型的層次關(guān)系.結(jié)合上述詞法層面的對應(yīng)原則，此時當(dāng)0≤j≤n，0≤i≤m時，S1中的變量的屬性信息A1對應(yīng)G1中的ξ1，b1.bsub1_j.bsub1_ji.A1=ξ1；S1中的P1對應(yīng)G1中的變量信息、事件信息和轉(zhuǎn)換信息，即：

b1.bsub1_j.bsub1_ji.P1=V1∪E1∪T1

(6)

S1中的C1對應(yīng)G1中的A1，即：

b1.bsub1_j.bsub1_ji.C1=A1

(7)

4.2 A2GTS算法總體框架

A2GTS算法主要由Block平展化算法、Class平展化算法和同步平展化算法三個算法組成，主要包括四個模塊，如圖3所示.具體步驟如下：

步驟1.利用ANTLR的元語言對AltaRica 3.0的語法規(guī)則進(jìn)行詳細(xì)的描述.獲取對應(yīng)的語法文件(altaRica.g4)，運行ANTLR內(nèi)置方法形成AltaRica的詞法和語法解析器，可以對一個AltaRica 3.0的實例進(jìn)行AST分析.

步驟2.對Block文件進(jìn)行層次化平展操作.首先對AltaRica 3.0模型文件進(jìn)行劃分，找出其主模塊Block和子模塊Block，其中主模塊Block是平展化程序入口；然后對主模塊Block的語法樹進(jìn)行層次遍歷，獲取其嵌套的第一層的Class信息和子模塊Block文件，將Block引用的Class信息存儲到對應(yīng)的GetClassMap數(shù)據(jù)結(jié)構(gòu)中，同時定義一個不定長的字符串s，將上一層Block的實例名加入到字符串s中.此時，字符串s就是當(dāng)前Block中元素的前綴標(biāo)識符，將Block平展化的信息存入到Bflat中，再次進(jìn)行層次遍歷和深度遍歷，重復(fù)上述的操作，直到獲取到最深的結(jié)點.

圖3 AltaRica 3.0平展化算法框架

步驟3.對Class文件進(jìn)行層次平展化操作.首先，根據(jù)步驟2獲取到的主模塊引用的Class信息，對GetClassMap數(shù)據(jù)結(jié)構(gòu)進(jìn)行遍歷，由GetClassMap中存放的Class類名和實例名，自動尋找到類名相同的Class文件建立的AST，實例名就是當(dāng)前Class的前綴標(biāo)識符，確定Class的所屬關(guān)系；然后獲取當(dāng)前Class文件引用的其他的Class文件信息，將Class類名和實例名存到對應(yīng)的GetClassMap中，再重復(fù)上述過程，直到確定所有的Class的前綴標(biāo)識符.

步驟4.對已經(jīng)平展化的層次化文件進(jìn)行同步事件平展化操作.AltaRica3.0模型文件的transition信息包含這個三種事件：正常事件，同步事件和隱藏事件，三者的關(guān)系就是包含關(guān)系，其中同步事件和隱藏事件包含正常事件.具體關(guān)系如圖4所示.

圖4 事件之間的相互關(guān)系

在已經(jīng)平展化文件形成的AST中，三種事件的存儲方式的主要區(qū)別就是其存儲結(jié)點的屬性信息的不同.首先，可以根據(jù)結(jié)點的屬性直接獲取對應(yīng)事件的類型，得到同步事件和隱藏事件子結(jié)點存儲的值(正常的轉(zhuǎn)換事件)；然后根據(jù)得到的值，遍歷AST，得到對應(yīng)事件包含的表達(dá)式和指令；再依據(jù)同步的平展化規(guī)則和隱藏的平展化規(guī)則對事件中的表達(dá)式和指令進(jìn)行操作，得到平展化后的同步事件和隱藏事件.

通過步驟2和步驟3 的不斷迭代就能獲取到嵌套層次結(jié)構(gòu)的平展化的文件，完成垂直方向的平展化(結(jié)構(gòu)層次的平展化)，步驟4完成水平方向的平展化過程(同步過程的平展化).

4.3 AltaRica 3.0模型的語法解析過程

4.3.1 構(gòu)建AltaRica 3.0的ANTLR語法模型

AltaRica模型是模型元素的集合，塊、類、常量、域、記錄和函數(shù)(blocks，classes，constants，domains，records and functions).其中基本元素是塊Block和類Class.模型元素可以在聲明之前使用.

Block或Class的內(nèi)部元素可以按任何順序聲明，但必須在transition和assertion之前聲明.Block或Class的內(nèi)部元素的聲明是不同的.inheritance(規(guī)則′ExtendsClause′)，variables，events，parameters，observers在塊和類中都能被定義，剩下的只能在塊中定義的是：aggregation(規(guī)則EmbedsClause)和clone(規(guī)則ClonesClause).

根據(jù)AltaRica 3.0的整體架構(gòu)，ANTLR可以將AltaRica3.0的結(jié)構(gòu)信息劃分為：1)詞法結(jié)構(gòu)定義，規(guī)定AltaRica 3.0中基本的構(gòu)造元素；2)表達(dá)式定義，規(guī)定AltaRica 3.0中的符號，布爾和數(shù)字表達(dá)式；3)指令集定義，AltaRica 3.0中的指令規(guī)定具體的語法轉(zhuǎn)換規(guī)則，描述轉(zhuǎn)換和斷言中的具體的轉(zhuǎn)換動作；4)屬性定義，一些模型元素使用屬性的概念來定義一些特征；5)域定義，AltaRica 3.0中的域是命名常量的命名集.

由Block和Class的定義，AltaRica 3.0提供了層次模型的構(gòu)造過程，即將實際系統(tǒng)的模型表述為組件之間相互嵌套的多層次結(jié)構(gòu)，AltaRica 3.0的ANTLR元語言的概述說明如下所示.

literalValue:boolean1|integer|real|literalAttributeValue|pathIdentifier;//詞法結(jié)構(gòu)定義expression:expressionnOperatorexpression|uOperatorex-pression|operatorCall|ifThenElseExpression|switchExpression|curve|literalExpression;//表達(dá)式定義instruction:skipSituation|halfEquivalentSituation|allEquivalentSituation|ifSituation|switchSitu-ation|multiInstructionSituation|identifierSit-uation;//指令集定義attributes:′(′attribute(′,′attribute)?′)′;//屬性定義domainDeclaration:′domain′identifier′{′symbolicConstants′}′;//域定義blockDeclaration:′block′identifier(blockDeclarationClause_get)?(blockDeclarationClause)?(transitionsClause)?(assertionClause)?′end′;//塊定義classDeclaration:′class′identifier(includeblockDeclarationClause_get)?(declarationClause)?(transitionsClause)?(assertionClause)?′end′;//類定義

4.3.2 生成AST示例

對AltaRica 3.0的ANTLR的語法解析文件的正確性進(jìn)行驗證.通過輸入一段實際的AltaRica 3.0的代碼進(jìn)行驗證，將代碼輸入到解析文件形成的詞法和語法分析器中，如果解析文件正確，詞法和語法分析器就會自動的識別輸入代碼的結(jié)構(gòu)，形成一棵抽象語法樹.輸入圖2(b)中描述的部分AltaRica 3.0模型語言，自動生成如圖7所示的AST，證明AltaRica 3.0的ANTLR的語法解析文件是正確.

圖5 AltaRica 3.0模型的語法樹

4.4 Block平展化算法處理

Block的平展化過程.定義一個Block由八元組構(gòu)成，B=，CE為Block中引用的類的信息(包括類名和實例名)；BM為聲明塊，是主模塊的說明，為整個AST樹的入口文件；BS為主模塊中嵌入的子塊和對象；D為聲明元素(變量，事件，參數(shù)和觀察者)；TM為主模塊的轉(zhuǎn)換；AM為主模塊的斷言；TS為子模塊的轉(zhuǎn)換；AS為子模塊的斷言.

使用“.”來標(biāo)識平展化過程中子組件的變量之間的所屬關(guān)系.例如，BM中，子塊BS的實例化對象為b，對象b中包含變量v，可以將其表述為b.v.以直觀的方式將“點符號”擴(kuò)展到變量集(即，如果V是一組聲明元素，則b.V={b.v|v∈D})，定義FlatB()用于對BM進(jìn)行平展化操作的遞歸函數(shù)，并使用FlatSonB()函數(shù)對子模塊BS中嵌套的子模塊的進(jìn)行平展操作.如果B是BM中的主模塊的信息，用B[Bi]來表示子模塊BS中嵌套的子模塊平展化的信息，用φ表示嵌套的層數(shù).另外，用ChildEle(B)表示B的嵌套的模塊集合.

FlatB(B)=

(8)

第一種情況：嵌套的層數(shù)為0，B表示主模塊中的信息，直接可以作為平展化的文件信息；

第二種情況：主模塊BM的嵌套層數(shù)只有一層，此時要調(diào)用FlatB()進(jìn)行平展化獲取轉(zhuǎn)換后的信息；

第三種情況：主模塊BM的嵌套層數(shù)大于一層，此時首先要調(diào)用FlatSonB()對子模塊BS中嵌套的模塊Bλ進(jìn)行平展化操作，然后再利用FlatB()進(jìn)行平展化操作.

可以將經(jīng)過平展化操作后的Block表述為一個四元組，即：

Bflat=

(9)

其中，模塊信息B′M由主模塊BM和平展化的子模塊BS構(gòu)成，即：

B′M=BM∪(∪{b′s|b′s=FlatB(bs)，bs∈BS})

(10)

聲明元素D′為子模塊中聲明元素(要經(jīng)過平展化操作)和主模塊中聲明元素的集，即：

D′=BS_Name.D∪BM.D

(11)

轉(zhuǎn)換轉(zhuǎn)換T′M為子模塊中轉(zhuǎn)換(要經(jīng)過平展化操作)和主模塊中轉(zhuǎn)換的集合，即：

T′M=BS_Name.TS∪BM.TM

(12)

斷言A′M為子模塊中斷言(要經(jīng)過平展化操作)和主模塊中斷言的集合，即：

A′M=BS_Name.AS∪BM.AM

(13)

Block平展化算法是一個迭代形式的算法，輸入Block的層次化語言，輸出文本形式的平展化的文本Bflat，和Block引用的Class類的信息(存放在GetClassMap).Block平展化算法偽代碼如算法1所示，第7到43行是一次完整的迭代過程.

算法1.Block平展化算法偽代碼

輸入：Block文件

輸出：已層次化扁平化的Block文件和引用Class信息

1.functionFLATTENBLOCK(B，Bflat)

2.Bflat←?;

3.Map>map←?;

4.v←?;

5.s←?;

6.ast←ANTLR.getAST(altarica.g4);

7.functionFlattenIncludeBlock(B，Bflat)

8.ASTB←ast.ParseTreeWalk(B);

9.ifB∈BMthen

10.v← ?;

11.elseifB∈BSthen

12.v←StringAppendBlockName(v，ASTB.getBlockName());

13.s←v;

14.endif

15.

16.functionGetContextFromMainAndSub(v，ASTB);

17.Bflat.add(v+ASTB.D);

18.forc∈CEdo

19.ifc.ClassNameis not inmap.keythen

20.map.key←c.ClassName;

21.map.get(key)←v+c.ObjectName;

22.else

23.map.get(c.ClassName)←v+c.ObjectName;

24.endif

25.endfor

26.

27.forallb∈Bdo

28. ifb∈BMthen

29.FlattenIncludeBlock(b，bflat，v);

30.bflat.add(Tm);

31.bflat.add(Am);

32.Bflat.add(bflat);

33.elseifb∈BSthen

34. FlattenIncludeBlock(b，bflat，s);

35.bflat.add(AddPrefixVariableAndEvent(s，b.D));

36.bflat.add(AddPrefixTransition(s，b.TS));

37.bflat.add(AddPrefixAssertion(s，b.AS));

38.Bflat.add(bflat);

39.endif

40.endfor

41.returnmap，Bflat;

42.endfunction

43.endfunction

44.endfunction

步驟1.對主模塊Block中的聲明元素D，CE，TM和AM進(jìn)行平展化的操作.I，G，P，Q分別為D，CE，TM和AM的數(shù)量，遍歷遞歸樹的根結(jié)點(即主Block)，根據(jù)平展化的規(guī)則，對于所有的Di，TMp和AMq不用添加前綴標(biāo)識符，可以直接放入到Bflat1中，即：

Bflat1={ψ|ψ.add(Di，TMp，AMq)，i∈I，p∈P，q∈Q}

(14)

當(dāng)j∈G時，將CEj放入GetClassMapM中，CEj.ClassName作為key，getKey:keyj←CEj.ClassName表示將引用的類名作為鍵的過程，由于一個類可以被多次實例化使用，因此將對應(yīng)的value定義為一個不定長的數(shù)組，存放引用的CEj.ObjectName;Λ為每個key對應(yīng)的value中引用類的數(shù)量，當(dāng)l∈Λ時，getValue:valuej∪{CEj.ObjectNamel}表示獲取所有鍵名為CEj.ObjectName對應(yīng)的value的過程，即：

(15)

步驟2.確定每一層子模塊BS的前綴標(biāo)識符.主模塊中包含子模塊BS，BS模塊又可包含BS，形成一棵遞歸樹.步驟二就是確定子模塊之間的所屬關(guān)系，將遞歸AST的層次深度作為循環(huán)條件，對于每一層BS進(jìn)行操作，由于子塊可以進(jìn)行多層嵌套，對于每一層塊的實例名都能作為下一層Block的前綴標(biāo)識符，前綴標(biāo)識符會隨著嵌套結(jié)構(gòu)和樹的深度的增加而逐層進(jìn)行記錄，算法中使用StringAppendBlockName()的方法進(jìn)行記錄.

步驟3.對子模塊Block中的聲明元素D，CE，TS和AS進(jìn)行平展化的操作.R為子Block的數(shù)目，對于某個聲明的子塊BS，其D，CE，TS和AS的數(shù)目分別為I，G，P，Q.第27行到40行是嵌套的子模塊的遞歸平展化過程，F(xiàn)lattenIncludeBlock()為一個遞歸函數(shù)，對所有的子塊進(jìn)行操作.同一個Block根結(jié)點的Block子結(jié)點的前綴標(biāo)識符都是相同的，對于一個Block根結(jié)點，其StringAppendBlockName()都是唯一的，并且只在這個子樹中起作用.當(dāng)r∈R時，就能獲取的每一層每一個子Block的前綴標(biāo)識符s，利用AddPrefixVarableAndEvent()方法對子Block的聲明元素D添加前綴標(biāo)識符s，即：

getD:AddPrefixVarbleAndEvent(s，BSr.Di)

(16)

每個子模塊的TS添加前綴標(biāo)識符s，即：

getT:AddPrefixTransition(s，BSr.TSp)

(17)

每個子模塊中的AS添加前綴標(biāo)識符s，即：

getA:AddPrefixAssertion(s，BSr.TSp)

(18)

將轉(zhuǎn)換后的Block的D，TS和AS平展化文件添加到Bflat2中，即：

Bflat2={ψ|ψ.add(getD，getT，getA)，i∈I，p∈P，q∈Q}

(19)

再把每一層BS引用的類的信息添加到GetClassMap中，重復(fù)第一步中添加引用類信息的過程.

4.5 Class平展化算法處理

Class的平展化過程.定義一個Class由一個五元組組成C=，CE為Class中引用的其他類的信息(包括類名和實例名)；BC為聲明塊，Class中引用的Block的說明；D為聲明元素(變量，事件，參數(shù)和觀察者)；T為Class中包含的轉(zhuǎn)換；A為Class中包含的斷言.

類的平展化和塊的平展化過程類似，F(xiàn)latC()為對Class進(jìn)行平展化操作的遞歸函數(shù).首先對Class中的聲明元素D，轉(zhuǎn)換T和斷言A進(jìn)行平展化操作；然后對當(dāng)前Class中引用的其他Class信息進(jìn)行遞歸操作，其中c是一個Class的實例化對象，即：

(20)

五元組Cflat=表示平展化后的Class文件，c.ObjectName為Class實例化對象的名稱，B′為Class中引用的Block的平展化后的信息；D′=c.ObjectName.D，D′為Class中平展化后的聲明元素；T′=c.ObjectName.T，其中T′為Class平展化后的轉(zhuǎn)換，A′=c.ObjectName.A，A′為平展化后的斷言.即：

(21)

Class平展化算法是一個遞歸形式的算法，F(xiàn)lattenClass()為一個遞歸函數(shù)，對所有的類進(jìn)行平展化操作.輸入Class的層次嵌套語言，輸出Class的引用類信息和平展化的Class文件.Class平展化算法的偽代碼如算法2所示.

算法2.Class平展化算法偽代碼

輸入：Class文件和引用的Class信息；

輸出：已經(jīng)層次化扁平的Block文件；

1.functionFlattenClass(C，Cflat，map);

2.Cflat←?;

3.ast←ANTLR.getAST(altarica.g4);

4.ASTC←ast.ParseTreeWalk(C);

5.forallB∈BAdo

6.FlattenBlock(b，bflat);

7.Cflat.add(bflat);

8.endfor

9.

10.forall∈mapdo

11.forallc∈Cdo

12.ifkey==c.getClassNamethen

13.foralls∈c.get(key)do

14.Cflat.add(AddPrefixVariableAndEvent(s，c.D));

15.Cflat.add(AddPrefixTransition(s，c.T));

16.Cflat.add(AddPrefixAssertion(s，c.A));

17.endfor

18.endif

19.endfor

20.endfor

21.map=new Map>();

22.fork ∈CEdo

23.ifk.ClassNameisnotinmap.keythen

24.map.key←k.ClassName;

25.map.get(key)←k.ObjectName;

26.else

27.map.get(k.ClassName)←k.ObjectName;

28.endif

29.endfor

30.forallp∈Cdo

31. FlattenClass(p，pflat，map);

32.Cflat.add(pflat);

33.Bflat.add(Cflat);

34.endfor

35.returnBflat;

36.endfunction

Class平展化算法具體步驟如下：

步驟1.Class文件的層次結(jié)構(gòu)的平展化.首先獲取所有的Class的AST，根據(jù)算法1對Class中引用的Block進(jìn)行平展化操作；其次根據(jù)算法1獲取的GetClassMap的key，尋找到類名和key相同的AST，以及對應(yīng)key下對應(yīng)的value，獲取GetClassMap中引用類的數(shù)量K；然后對該AST進(jìn)行深度優(yōu)先遍歷，獲取到對應(yīng)類中所有的D，T，A，其D，CE，T和A的數(shù)目分別為I，H，P，Q，當(dāng)k∈K時，對Class中的聲明元素D添加前綴標(biāo)識符，即：

getD:AddPrefixVableAndEvent(vauek，Ck.Di)

(22)

對每個Class中的轉(zhuǎn)化信息T添加前綴標(biāo)識符，即：

getT:AddPrefixTransition(valuek，Ck.Tp)

(23)

對每個Class中的斷言信息A添加前綴標(biāo)識符，即：

getA:AddPrefixTransition(valuek，Ck.Ap)

(24)

(25)

Bflat_hier=B′flat∪B″flat

(26)

步驟2.獲取每個Class文件的引用的Class的信息.遍歷當(dāng)前Class的AST，找到當(dāng)前Class的CE信息，重復(fù)上述遞歸函數(shù)FlattenClass()的過程，直到找到不引用其他類的Class，遞歸過程結(jié)束.

在類和塊的平展化的過程中，轉(zhuǎn)換和斷言也存在對應(yīng)的嵌套遞歸結(jié)構(gòu)，由AltaRica 3.0語法定義的ANTLR語法文件altarica.g4可知，轉(zhuǎn)換的主要形式為Ei:Qi->Pi，其中Ei為事件，Qi為表達(dá)式結(jié)構(gòu)，在altarica.g4中定義為expressions，對應(yīng)生成的AST的結(jié)點名稱也為expressions，其中Pi為指令結(jié)構(gòu)，在altarica.g4中定義為instruction，對應(yīng)生成的AST結(jié)點的名稱為instruction.

由4.2.1節(jié)的表達(dá)式和指令的解析過程，expressions中一共包含6種嵌套結(jié)構(gòu)，可以產(chǎn)生6n種可能的結(jié)構(gòu)，instruction一共包含5種嵌套結(jié)構(gòu)，而且每個嵌套結(jié)構(gòu)還和expressions結(jié)構(gòu)進(jìn)行嵌套，但是instruction和expressions生成遞歸的AST的過程是類似的，按照遞歸AST的遞歸原則(即expressions或instruction的語法嵌套規(guī)則)不斷的進(jìn)行遞歸，每遞歸一次，語法樹就增加一層，直到樹中結(jié)點的屬性為curve或literalExpression(即所有的結(jié)點都為Terminal葉子結(jié)點，存放具體的數(shù)值)，此時葉子結(jié)點的數(shù)值就是要進(jìn)行平展化的變量，算法2和算法3 的過程就是確定該變量的所屬關(guān)系.

4.6 同步平展化算法處理

同步(Sync)的平展化過程.該過程主要對已經(jīng)層次化平展化的Bflat_hier進(jìn)行同步的平展化操作.算法的偽代碼如算法3所示：

算法3.Sync的平展化算法偽代碼

輸入：所有已扁平化的文件；

輸出：已進(jìn)行同步扁平化和隱藏扁平化的文件；

1.functionFlattenClass(C，Cflat，map);

2.Syncflat←?;

3.ast←ANTLR.getAST(altarica.g4);

4.ASTBflat←ast.ParseTreeWalk(Bflat);

5.Map>mapGrandson←?;

6.MapmapSon←?;

7.Mapmap←?;

8.forallb∈AllSynNamedo

9.ifbisnotinmapGrandson.keythen

10.mapGrandson.key←b;

11.mapGrandson.get(key)←b.getEventInSyncName();

12.else

13.mapGrandson.get(b)←b.getEventInSyncName();

14.endif

15.endfor

16.

17.forallb∈mapGrandsondo

18.ifb.keyisnotinmapSon.keythen

19.mapSon.key←b.key;

20.ifb.get(key).getValue()==”strong”then

21.mapSon.get(”strong”).append(b.get(key));

22.elseifb.get(key).getValue()==”weak”then

23. mapSon.get(”weak”).append(b.get(key));

24.endif

25.endif

26.endfor

27.

28.forallb∈mapSondo

29.ifb.keyisnotinmap.keythen

30.map.key←b.key;

31.ifb.get(key).getValue()==”strong”then

32.map.get(”ins”).append(b.getInstruction());

33.map.get(”exp”).append(b.getExpression());

34.elseifb.get(key).getValue()==”weak” then

35.map.get(”ins”).append(b.getInstruction());

36.map.get(”exp”).append(b.getExpression());

37.endif

38.endif

39.endfor

40.

41.forallb∈mapdo

42.Syncflat.add(TranslateSyncInRule(b));

43.Bflat←Bflat∪Syncflat;

44.endfor

45.returnBflat;

46.endfunction

Sync的平展化算法最重要的步驟就是遍歷已經(jīng)層次平展化的語法樹ASTBflat.由3.2.1節(jié)的轉(zhuǎn)換模塊的ANTLR解析的過程，同步事件中transition和individualTransition只能包含一層循環(huán).同步轉(zhuǎn)換的形式為e：!a1&…&!aM&?b1&…&?bn&L1→R1& …&Lr→Rr，(m≥0，n≥0，r≥0，!為強(qiáng)同步事件，?為弱同步事件，Lr為布爾表達(dá)式，Rr為指令)，平展化的過程是對a1，…，an，b1，…，bm中包含的表達(dá)式和指令信息進(jìn)行轉(zhuǎn)換.

步驟1.取出同步事件中包含的正常事件.首先遍歷ASTBflat，根據(jù)樹結(jié)點的屬性獲取其中的同步事件，為同步事件的數(shù)量，getSyn:keyφ←SynEventφ；取同步事件中的正常事件，M為正常事件的數(shù)量，normalEventλ是同步事件e中的[a1，…，an，b1，…，bm]，λ∈M時，即：

getNormal:valueφ∪{normalEventλ}

(27)

然后就可以將e，[a1，…，an，b1，…，bm]的形式擴(kuò)展為一個map映射，在算法中定義的是mapGrandson用于存放同步事件和同步事件中的正常事件，即：

(28)

步驟2.獲取正常事件包含的表達(dá)式和指令信息.首先通過mapGrandson中包含的正常事件對語法樹ASTBflat進(jìn)行再次遍歷，根據(jù)3.2節(jié)中轉(zhuǎn)換事件的定義，強(qiáng)弱同步事件的內(nèi)容直接由expressions和instruction組成，獲取到屬性為expressions和instruction的結(jié)點；然后遍歷到葉子結(jié)點，獲取到包含的內(nèi)容，存入到mapSon中.

步驟3.獲取平展化后的事件.由同步的平展化規(guī)則，主要針對第二步中獲取的mapSon中存儲的expressions和instruction進(jìn)行相應(yīng)的操作.算法首先利用同步的平展規(guī)則函數(shù)，即TranslateSyncRule()對mapSon的內(nèi)容進(jìn)行操作，將平展化的結(jié)果放入mapAll中；然后遍歷mapAll的內(nèi)容，和之前進(jìn)行層次平展化的文件(不包括未平展化的同步事件)合并，得到相應(yīng)的平展化文件；其次由hide的規(guī)則進(jìn)行相應(yīng)的隱藏操作，由此平展化過程執(zhí)行完畢；最后輸出經(jīng)過隱藏操作后的平展化文件，即：

Bflat=Bflat_hier∪Bflat_syn_hide

(29)

4.7 算法分析

4.7.1 算法時間復(fù)雜度分析

通過實驗數(shù)據(jù)可得整個算法的時間消耗發(fā)生在算法1和算法2的遞歸，以及Block和Class中轉(zhuǎn)換和斷言的嵌套遞歸上：

第一，主模塊Block中的子模塊Block的嵌套遞歸.假設(shè)一個Block中能嵌套m個子模塊Block，則嵌套的子模塊Block最多有mn-1個，其中n為主模塊文件形成的AST樹的層數(shù)(即最多的嵌套層數(shù)可以達(dá)到n層)，而且每個Block嵌套的子Block的數(shù)目可能不一樣，m是最大嵌套數(shù)的情況.

對算法1的時間復(fù)雜度分析可以直接看成對形成的遞歸AST樹的時間分析，初始的遞歸樹只有一個結(jié)點，主模塊的權(quán)值標(biāo)記為T(n)，然后按照遞歸樹的遞歸規(guī)則不斷地進(jìn)行遞歸，每遞歸一次遞歸樹增加一層，直到獲取到最大深度的子模塊Block所在的層.由于在實際的應(yīng)用過程中，一個系統(tǒng)是由有限個子系統(tǒng)組成，所以可以設(shè)置一個衰減函數(shù)T(n/b)，限定子模塊的數(shù)量，規(guī)定最深層的Block的權(quán)值標(biāo)記為T(1)，由此可以得到一個遞歸方程：

分析可知其時間復(fù)雜度為O(nlogbm).

第二，在引用類的嵌套上，假設(shè)每個Block能引用k個Class，每個Class最多可以擴(kuò)展c個Class，則每個Block最多可以包含k×cr個Class，其中r為遍歷到的無引用擴(kuò)展類的最大樹的深度，此時也是對一個遞歸樹進(jìn)行分析，此時算法2 的時間復(fù)雜度為O(k×rlogbc).

第三，同步的平展化過程，主要是線性分析，假設(shè)每個同步事件都有t個強(qiáng)弱事件組成，則依次對這t個事件進(jìn)行分析，相應(yīng)的時間復(fù)雜度為O(t).

4.7.2GetMapClass數(shù)據(jù)結(jié)構(gòu)

GetMapClass數(shù)據(jù)結(jié)構(gòu)由隊列和map映射組成，將Block和Class的平展化過程有效的進(jìn)行分割，降低整個算法的復(fù)雜度.平展化算法的入口主模塊Block包含了初始遞歸條件.如果在ANTLR的遍歷過程中，遍歷到其中引用的類，就開始查找引用類的AST，此時就變成多棵樹同時進(jìn)行遍歷查找.從結(jié)構(gòu)上來說，這個過程可看成是主模塊Block的AST和引用類的AST進(jìn)行了合并，形成了更大的一棵存在嵌套遞歸結(jié)構(gòu)的AST.分析可知，對該AST進(jìn)行相應(yīng)的平展化操作，無疑會增加額外的時空開銷.

對此，本節(jié)提出Block和Class之間的傳值結(jié)構(gòu)GetMapClass，使Block和Class之間的平展化操作在空間上不會相互影響.對于建立的Block樹，利用設(shè)計的遍歷算法對Block進(jìn)行有效的平展化操作.在遍歷過程中，不會有停頓操作，對于Block中引用的類，會自動放入到GetMapClass數(shù)據(jù)結(jié)構(gòu)中，保證Block的遍歷能一直到最深Block所在的層次.同時，對于屬于同一根結(jié)點的子Block，利用隊列的功能進(jìn)行關(guān)系標(biāo)注，確保屬于同一根結(jié)點的子Block的前綴標(biāo)識符相同.最后利用GetMapClass進(jìn)行傳值操作，根據(jù)GetMapClass中包含的引用信息自動找到已經(jīng)建立的Class的AST，取出GetMapClass中包含的value信息，對Class進(jìn)行相應(yīng)的平展化操作的同時，將當(dāng)前Class中包含的引用類信息加入到GetMapClass，直到GetMapClass中不包含任何信息(即，遍歷到不包含任何引用信息的Class)，同時層次結(jié)構(gòu)的平展化過程結(jié)束.

4.7.3 AST遍歷算法設(shè)計

層次平展化最重要的過程是獲得最外層模塊和內(nèi)層模塊之間的所屬關(guān)系，確定它們各自的前綴標(biāo)識符.模塊之間層次結(jié)構(gòu)可以利用AST進(jìn)行表示，對整個AST樹進(jìn)行遍歷獲得當(dāng)前模塊的前綴標(biāo)識符.

根據(jù)AST的特性，一個父模塊可能包含多個子模塊，此時的遍歷方法宜采用層次遍歷的方法，而根據(jù)前綴標(biāo)識符的規(guī)則確認(rèn)這宜于采用深度遍歷的方法.結(jié)合上述兩種特性，A2GTS算法將深度遍歷和層次遍歷相結(jié)合，對整棵AST自上而下進(jìn)行遍歷，獲取相應(yīng)的前綴標(biāo)識符，而對于隸屬于一個父模塊的子模塊進(jìn)行層次遍歷，確定子模塊中所有組件的前綴標(biāo)識符.然后將所有的子模塊確定為父模塊，分別尋找它們所屬的子模塊，重復(fù)以上過程，直到所有的Block都不包含任何的子模塊，整個遍歷過程結(jié)束.

5 實驗結(jié)果和分析

本節(jié)主要描述算法的工具架構(gòu)設(shè)計，并對算法的有效性進(jìn)行驗證.對四個不同復(fù)雜度的AltaRica 3.0模型進(jìn)行實驗分析，將A2GTS算法實現(xiàn)平展化獲取的結(jié)果和實際的平展化文件相比較，驗證得到結(jié)果的正確性.

5.1 實驗描述和環(huán)境

實驗采用3.2節(jié)所描述的冷卻系統(tǒng)(CoolingSystem)、文獻(xiàn)[22]中的機(jī)輪剎車系統(tǒng)(WBS)、文獻(xiàn)[23]中的供電系統(tǒng)(ElectricalSystem)和文獻(xiàn)[20]中的灌溉系統(tǒng)(IrrigationSystem)進(jìn)行平展化算法的驗證.表1中從左向右，每列分別表示Block的嵌套層數(shù)、Class的引用層數(shù)、Block數(shù)量和Class數(shù)量.

表1 AltaRica 3.0模型信息

Table 1 AltaRica 3.0 model information

模型Block嵌套層數(shù)Class引用層數(shù)Block數(shù)量Class數(shù)量WBS15115CoolingSystem2344ElectricalSystem4465IrrigationSystem3343

本實驗運用基于ANTLR的AltaRica 3.0的平展化算法A2GTS對四個模型進(jìn)行平展化操作，四個模型的主要區(qū)別是Block和Class的嵌套層不同，以驗證在不同的主樹嵌套復(fù)雜度的情況下整個算法的平展化效率.

表2 不同的模型在平展化過程中的內(nèi)存和時間消耗

Table 2 Memory and time consumption of different models during flattening

模型遍歷深度時間消耗(ms)內(nèi)存消耗(KB)WBS61365038521CoolingSystem5966932076ElectricalSystem81455140124IrrigationSystem61374039551

本文所涉及的試驗數(shù)據(jù)均是在一臺CPU為Intel(R)Xeon(R)CPU E5-1603 0 @ 2.80GHz、內(nèi)存為8GB、操作系統(tǒng)為Windows 10 Enterprise的計算機(jī)上得到的，算法利用Java語言實現(xiàn)，實驗的消耗信息如表2和圖8所示.

由于篇幅限制，僅選取冷卻系統(tǒng)和灌溉系統(tǒng)的平展化結(jié)果進(jìn)行說明，實驗的結(jié)果信息如圖6和圖7所示，本文所用到的模型說明，平展化結(jié)果和平展化過程在網(wǎng)盤中展示1.

5.2 實驗結(jié)果和分析

對圖6和圖7分析，圖6詳細(xì)的描述了3.2節(jié)描述的冷卻系統(tǒng)的組件的平展化信息，每個泵類Pump的失效事件failure和修復(fù)事件repair均用其所屬關(guān)系進(jìn)行表示(LineOne.POne.failure，LineTwo.PTwo.repair等)，變量的信息也被完整地表述出來，水箱類Tank的空事件getEmpty在GTS中仍然保持只被Tank類所有(T.getEmpty).A2GTS將冷卻系統(tǒng)的多層次復(fù)雜結(jié)構(gòu)在一層模型上進(jìn)行了很好地描述，也表示出了組件之間的流變量的交互(LineOne.POne.inFlow，LineTwo.PTwo.inFlow)等，同時冷卻系統(tǒng)的層次信息保持不變.圖7分析過程類似.

圖6 平展化的冷卻系統(tǒng)

圖7 平展化的灌溉系統(tǒng)

圖8 A2GTS算法平展化消耗信息

1https：//pan.baidu.com/s/1UB7dHeSS25pTZMqkGuF5yQ

由圖6和圖7分析可知，A2GTS可以完成復(fù)雜的多層次嵌套結(jié)構(gòu)的AltaRica 3.0模型的平展化過程，對冷卻系統(tǒng)進(jìn)行平展化操作得到的結(jié)果和圖3所示的實際平展化系統(tǒng)主要差別是在于平展文件的顆粒度不同，實際平展化的系統(tǒng)模型可以將具有相同屬性的變量或者事件合并，而A2GTS算法得到的結(jié)果是將每個變量和事件單獨說明，相比于原來的平展化系統(tǒng)，A2GTS得到的結(jié)果更加的詳細(xì).由表2和圖8分析可知，算法的主要時間消耗和內(nèi)存消耗在整個AltaRica 3.0系統(tǒng)的層次結(jié)構(gòu)復(fù)雜度上，具體是Block的嵌套層數(shù)和Class的引用層數(shù)，層數(shù)越多，遍歷深度就越深，A2GTS消耗的時間和內(nèi)存也就越多.下一步可以針對復(fù)雜的多層的AltaRica 3.0模型系統(tǒng)通過初步的平展化操作減少層數(shù).例如將第一層的組件信息直接剝離，剩下內(nèi)部包含的系統(tǒng)組件信息，這樣就減少一層嵌套信息，從而降低了空間復(fù)雜度，這也是本文下一步的工作內(nèi)容.

6 結(jié)論和展望

本文主要工作包括：首先對整個AltaRica 3.0模型進(jìn)行語法解析，根據(jù)AltaRica 3.0語法規(guī)則定義AltaRica 3.0的ANTLR元語言文件，通過ANTLR的內(nèi)置方法對AltaRica 3.0的元語言進(jìn)行解析，得到其語法解析器和詞法解析器；其次，對輸入的某個實際的AltaRica 3.0模型系統(tǒng)按照Block和Class進(jìn)行分割，分別提出其中的Block和Class信息部分，將信息以字符流的形式輸入到詞法和語法解析器中，獲取到字符流中的詞法和語法信息，建立對應(yīng)Block和Class的AST；然后根據(jù)設(shè)計的算法對這兩個語法樹進(jìn)行操作，獲取結(jié)點信息，利用已經(jīng)制定的平展化的規(guī)則和算法，不斷地遞歸獲取平展化信息，得到最終的GTS平展化模型信息.

目前A2GTS算法的版本已經(jīng)能夠完成對一般AltaRica 3.0模型的分析和平展化，進(jìn)一步的研究工作包括：第一，AltaRica 3.0的ANTLR元語言顆粒度細(xì)化定義，顆粒度問題要在實際的工程系統(tǒng)應(yīng)用過程中，按照實際的語法規(guī)則識別需求進(jìn)行顆粒度的細(xì)化，實現(xiàn)語法解析的精確定位；第二，增加對大規(guī)模層次系統(tǒng)的分析，提高算法通用性；第三，設(shè)計AltaRica 3.0模型到NuSMV模型的轉(zhuǎn)換算法，應(yīng)用模型檢驗技術(shù)來進(jìn)行形式化分析；第四，A2GTS算法暫時還不能識別domain中的符號常量，是下一步算法改進(jìn)的方向.第五，進(jìn)行GTS模型的故障樹自動生成的研究.