基于ANTLR的AltaRica 3.0模型平展化算法設計與實現

陳 朔，胡 軍，王立松

1(南京航空航天大學 計算機科學與技術學院，南京 211106) 2(軟件新技術與產業化協同創新中心，南京 210007)

1 引 言

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

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

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

2 相關工作

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

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

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

3 ANTLR與AltaRica 3.0概述

3.1 ANTLR概述

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

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

圖1 ANTLR解析過程

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

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

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

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

4)自定義轉換過程：通過制定的轉化規則，就可以對獲取的文本信息進行相應的轉換，產生特定的輸出文本，獲取到轉換后的文件.

3.2 AltaRica 3.0模型

AltaRica 3.0是基于事件的建模語言，主要由系統結構建模語言S2ML和衛士轉換系統GTS組成[20]，其中S2ML是描述AltaRica 3.0的層次結構的模型語言，GTS則用來對AltaRica 3.0進行安全分析的形式化語義模型.

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

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

圖2

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

GTS是一類支持安全分析的狀態/轉換形式的模型，可以用來表示具有即時環路的系統，描述系統組件在環路中的狀態轉換.GTS對系統進行描述的模型稱為平展化的模型，AltaRica 3.0多層次模型轉換為GTS模型的過程稱為平展化操作.圖2冷卻系統的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的多層次結構模型S2ML進行平展化處理，利用面向對象的思想，將多個類編譯成一個GTS模型，其中變量、參數、觀察變量、事件按照調用關系重新命名，例如主類main中有一個對象a，a中有一個對象b，b中有一個變量s，那么s在GTS中可表示為a.b.s，例如Reactor中的inFlow變量在GTS中被表述為Reactor.inFlow，通過這種方式，AltaRica 3.0模型的層次結構信息被完整表達，但是對應的GTS模型只有一層結構，從而簡化了整個模型的層次結構.

使用AltaRica 3.0模型描述的某復雜結構的系統模型都可以轉換成等效的平展化GTS模型.本文根據AltaRica 3.0和GTS的語法規則，制定了相應的轉換規則，設計了一套轉換算法A2GTS，實現AltaRica 3.0模型自動轉換成為對應的GTS平展化模型.

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

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

4.1 形式化轉換過程

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

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

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

定義2.衛士轉換系統(GTS)是一個五元組[20]：

G=

(1)

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

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

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

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

?ξ是V的變量分配，是對狀態變量和流變量的初始賦值，其中狀態變量的初始化的關鍵字為“init”，流變量的初始化的關鍵字為“reset”.

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

ε(G)=TRUE

(2)

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

定義3.系統結構建模語言(S2ML)是一個四元組：

S=

(3)

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

?P(Ports)代表系統中組件的抽象類信息，AltaRica 3.0利用面向對象的思想將真實系統中的組件進行抽象，端口是模型的基本對象，包括variables，events和transitions，即：

P=Pv∪Pe∪Pt

(4)

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

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

B=BP∪BC∪Bsub

(5)

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

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

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

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

(6)

S1中的C1對應G1中的A1，即：

b1.bsub1_j.bsub1_ji.C1=A1

(7)

4.2 A2GTS算法總體框架

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

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

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

圖3 AltaRica 3.0平展化算法框架

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

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

圖4 事件之間的相互關系

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

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

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

4.3.1 構建AltaRica 3.0的ANTLR語法模型

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

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

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

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

literalValue:boolean1|integer|real|literalAttributeValue|pathIdentifier;//詞法結構定義expression:expressionnOperatorexpression|uOperatorex-pression|operatorCall|ifThenElseExpression|switchExpression|curve|literalExpression;//表達式定義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的語法解析文件的正確性進行驗證.通過輸入一段實際的AltaRica 3.0的代碼進行驗證，將代碼輸入到解析文件形成的詞法和語法分析器中，如果解析文件正確，詞法和語法分析器就會自動的識別輸入代碼的結構，形成一棵抽象語法樹.輸入圖2(b)中描述的部分AltaRica 3.0模型語言，自動生成如圖7所示的AST，證明AltaRica 3.0的ANTLR的語法解析文件是正確.

圖5 AltaRica 3.0模型的語法樹

4.4 Block平展化算法處理

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

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

FlatB(B)=

(8)

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

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

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

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

Bflat=

(9)

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

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

(10)

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

D′=BS_Name.D∪BM.D

(11)

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

T′M=BS_Name.TS∪BM.TM

(12)

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

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進行平展化的操作.I，G，P，Q分別為D，CE，TM和AM的數量，遍歷遞歸樹的根結點(即主Block)，根據平展化的規則，對于所有的Di，TMp和AMq不用添加前綴標識符，可以直接放入到Bflat1中，即：

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

(14)

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

(15)

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

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

getD:AddPrefixVarbleAndEvent(s，BSr.Di)

(16)

每個子模塊的TS添加前綴標識符s，即：

getT:AddPrefixTransition(s，BSr.TSp)

(17)

每個子模塊中的AS添加前綴標識符s，即：

getA:AddPrefixAssertion(s，BSr.TSp)

(18)

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

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

(19)

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

4.5 Class平展化算法處理

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

類的平展化和塊的平展化過程類似，FlatC()為對Class進行平展化操作的遞歸函數.首先對Class中的聲明元素D，轉換T和斷言A進行平展化操作；然后對當前Class中引用的其他Class信息進行遞歸操作，其中c是一個Class的實例化對象，即：

(20)

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

(21)

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

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

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

輸出：已經層次化扁平的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文件的層次結構的平展化.首先獲取所有的Class的AST，根據算法1對Class中引用的Block進行平展化操作；其次根據算法1獲取的GetClassMap的key，尋找到類名和key相同的AST，以及對應key下對應的value，獲取GetClassMap中引用類的數量K；然后對該AST進行深度優先遍歷，獲取到對應類中所有的D，T，A，其D，CE，T和A的數目分別為I，H，P，Q，當k∈K時，對Class中的聲明元素D添加前綴標識符，即：

getD:AddPrefixVableAndEvent(vauek，Ck.Di)

(22)

對每個Class中的轉化信息T添加前綴標識符，即：

getT:AddPrefixTransition(valuek，Ck.Tp)

(23)

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

getA:AddPrefixTransition(valuek，Ck.Ap)

(24)

(25)

Bflat_hier=B′flat∪B″flat

(26)

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

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

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

4.6 同步平展化算法處理

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

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

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

輸出：已進行同步扁平化和隱藏扁平化的文件；

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

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

getNormal:valueφ∪{normalEventλ}

(27)

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

(28)

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

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

Bflat=Bflat_hier∪Bflat_syn_hide

(29)

4.7 算法分析

4.7.1 算法時間復雜度分析

通過實驗數據可得整個算法的時間消耗發生在算法1和算法2的遞歸，以及Block和Class中轉換和斷言的嵌套遞歸上：

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

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

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

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

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

4.7.2GetMapClass數據結構

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

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

4.7.3 AST遍歷算法設計

層次平展化最重要的過程是獲得最外層模塊和內層模塊之間的所屬關系，確定它們各自的前綴標識符.模塊之間層次結構可以利用AST進行表示，對整個AST樹進行遍歷獲得當前模塊的前綴標識符.

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

5 實驗結果和分析

本節主要描述算法的工具架構設計，并對算法的有效性進行驗證.對四個不同復雜度的AltaRica 3.0模型進行實驗分析，將A2GTS算法實現平展化獲取的結果和實際的平展化文件相比較，驗證得到結果的正確性.

5.1 實驗描述和環境

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

表1 AltaRica 3.0模型信息

Table 1 AltaRica 3.0 model information

模型Block嵌套層數Class引用層數Block數量Class數量WBS15115CoolingSystem2344ElectricalSystem4465IrrigationSystem3343

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

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

Table 2 Memory and time consumption of different models during flattening

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

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

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

5.2 實驗結果和分析

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

圖6 平展化的冷卻系統

圖7 平展化的灌溉系統

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

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

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

6 結論和展望

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

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