軟件體系結構的屬性圖文法描述及其約束驗證
2007-01-01 00:00:00石兵冉平馬曉星陶先平呂建
計算機應用研究 2007年3期
摘 要：在前人工作的基礎上，使用了一種利于約束檢查和屬性刻畫的屬性圖文法，該方法形式地描述了體系結構及其演化；接著給出了一個算法檢查演化動作是否會破壞體系結構約束。在對屬性圖文法系統AGG的圖形解析器進行定制和改進的基礎上，設計并實現了體系結構自動檢查器。該檢查器已應用于面向體系結構的服務集成開發平臺Artemis—ARC系統中。
關鍵詞：軟件體系結構； 動態演化； 屬性圖文法； 驗證
中圖分類號：TP311文獻標志碼：A
文章編號：1001—3695(2007)03—0163—06
0 引言
軟件體系結構是指該系統的構件組成、構件間的相互關系和連接方式所形成的系統結構配置及動機、模式和約束等[1]。動態軟件體系結構則是指系統運行時刻軟件體系結構可以演化，進行重配置。動態體系結構研究中，如何保證體系結構的演化不會破壞體系結構的約束是關鍵技術之一[2]。一般情況下，動態體系結構演化是在系統運行時刻進行的，因此體系結構約束驗證必須在線、自動進行。體系結構約束包括屬性值限制、體系結構拓撲限制等，它實際上給出了合法體系結構的集合。
體系結構約束驗證方法一般包括兩個部分，即約束描述和約束檢查算法。越來越多的機構和個人在動態體系結構演化及其約束驗證方面開展工作并取得良好成果，其中體系結構描述語言ACME使用一階謂詞邏輯作為約束描述語言。此外還引入函數表示體系結構的特定特征，在給出約束描述后，在Armani原型系統中實現了一個基于深度優先算法的體系結構檢查器[4，5]。其他一些動態體系結構描述語言，如Wright[6，7]、Darwin[8—10]等，均給出了約束描述和約束檢查算法。這些方法在完善性、直觀性、應用復雜性等方面不同程度地存在不足之處。例如ACME限制類型的表示，使得結構類型元素是一個有限集合，從而解決一階謂詞邏輯的不可判定性問題；Wright中對狀態機進行窮盡搜索，因此在時間和空間上存在限制；Darwin提供的編譯器尚不完善，有些違反約束的情況無法檢查出來。
Daniel Le Metayer[11]提出使用圖文法(Graph Grammar)形式地描述體系結構及其風格。文獻[13，14]提出了使用圖文法驗證體系結構是否滿足約束；這種基于圖文法的約束驗證方法優點在于直觀、易理解，并且圖文法還可對面向圖系統中的圖進行形式描述。但文獻[11，13，14]的工作還只是理論上的研究，沒有真正地實現，另外也沒有明確定義體系結構的屬性信息該如何描述和驗證。本文在文獻[11，13，14]的基礎上，討論了一種基于屬性圖文法的體系結構描述及約束驗證方法。基于屬性圖文法的體系結構描述方法不但刻畫了包括屬性在內的體系結構信息，還有利于使用圖形解析技術進行包括屬性在內的約束驗證。在此理論基礎上，利用屬性圖文法系統AGG[3]的圖形解析器設計和實現了體系結構自動檢查器，并將其應用于Artemis—ARC系統[1]中。該系統采用面向圖的運行時體系結構對象技術，該技術與屬性圖文法描述體系結構模型是一致的。體系結構的演化首先將被模擬執行；然后對模擬執行后的體系結構進行約束驗證；如約束滿足，則演化被真正執行，并能在約束滿足方面得到保障。
1 體系結構的屬性圖文法描述和約束驗證
1.1 體系結構的屬性圖文法描述
本文分別用體系結構實例屬性圖(AAG)、體系結構風格屬性圖文法(ASGG)來形式地描述體系結構實例、體系結構風格，用屬性圖轉換描述體系結構演化。它們的形式定義如下。
定義1 體系結構實例屬性圖。LVT是終結節點標記集合，LET是終結邊標記集合，基調(Signature) Sig=(S，OP)，則AAG=(V，E，s，t，lv，le，AAGA，av，ae)是基調為Sig的屬性圖，其中：
(1)V是有限個終結節點的集合；E是有限個終結邊的集合。
(2)s：E→V是源節點函數；t：E→V是目標節點函數。
(3)lv：V→LVT是終結節點標記函數；le：E→LET是終結邊標記函數。
(4)AAGA是一個Sig代數(Sig—Algebra)。
(5)av：V→U(AAGA)和ae：E→U(AAGA) 分別是終結節點和終結邊的屬性函數。
體系結構實例實際上包含了：
①構件(Component)和連接子(Connector)。
②構件和連接子組成的體系結構的配置信息。
③屬性信息。
AAG形式地描述了上述體系結構實例：
①體系結構實例中出現的構件com∈V、lv(com)表明了構件類型；連接子con∈E、le(con)表明了連接子類型。
②配置信息表現為V、E上的圖，函數s、t定義了拓撲結構。
③函數av：V→U(AAGA)和ae：E→U(AAGA)賦予體系結構實例屬性信息。
與屬性圖定義不同，AAG中節點和邊必須是終結的。當屬性圖中含有非終結元素時，它可能是某推導序列中的中間圖。中間圖定義與附錄中屬性圖定義一致。
與一般圖文法定義不同，ASGG進行了擴展，除了有初始圖和產生式集合外，還有節點標記、邊標記集合以及屬性指派，從而可以很好地形式描述體系結構風格。在上述ASGG定義中，屬性由基調Sig=(S，OP)來描述，還是抽象描述；在屬性圖中，具體屬性信息將由Sig代數描述。
體系結構風格實際上規定了：
（1）體系結構實例中出現的構件類型和連接子類型；
（2）上述類型的構件和連接子構造的體系結構實例所要滿足的拓撲結構約束、體系結構實例中構件和連接子要滿足的屬性約束。
也就是說，演化合法，即要保證演化后體系結構仍然遵循原體系結構風格，在屬性圖文法中就是要保證AAG′∈L(ASGG)成立。判斷它是否成立，形式語言中稱為從屬問題(Membership Problem)，是一個NP完全問題[17]。在一個受限圖文法中，這個問題是可以解決的，如基于圖形解析(Graph Parsing)技術，判斷待檢查圖是否可達(Reachable)。可達是指在圖形轉換系統中，待檢查圖不含非終結元素，從初始圖出發使用產生式經一系列推導得到的圖與待檢查圖同構[19] (在屬性圖文法中是屬性圖同構)。本文就是基于圖形解析技術進行約束驗證的，下面給出約束描述和約束驗證算法。
1.2 約束驗證
定義3 約束滿足。對于體系結構實例屬性圖，如果AAG′. AAG′∈L(ASGG) ∧ AAG′≌AGAAG，則AAG對于ASGG是約束滿足的。AAG描述的體系結構實例遵循ASGG描述的體系結構風格。
定義了約束滿足后，給出約束檢查算法。約束檢查算法基于圖形解析技術，判斷是否可找到合適的產生式序列，初始圖按此產生式序列進行推導保證待檢查圖可達。為了能讓算法正常終止，給出限制條件如下：
該條件要求產生式右部元素(節點、邊)不比左部少，至少創建或修改其中一個元素。它和算法中的回溯條件一起保證算法終止。在CHOMSKY文法體系中將滿足此限制條件的文法稱為1型文法，即上下文相關文法[20]。由于從初始圖進行圖形推導判斷待檢查圖是否可達，待檢查圖元素數一般大于初始圖或是對初始圖元素的修改，在推導過程中不會用到右部元素比左部少或左、右部圖同構的產生式，故該限制條件是合理的。約束檢查算法如下：
該算法是深度優先的回溯搜索算法。一般情況下回溯算法的可終止性和正確性是能得到保證的。當它用于語言解析時，要防止由于循環文法(Cyclic Grammar)[21]引起推導無限循環，造成檢查無法終止。前述限制條件雖然沒有防止循環文法的出現，但是在算法中采取了措施保證跳出循環，從而使算法可終止，正確性也可得到保證。
定理1 給定滿足前述限制條件的體系結構風格屬性圖文法和體系結構屬性圖，驗證AAG對于ASGG是否約束滿足。算法1總可以保證驗證過程是可終止的。
證明 用|G|表示圖中元素數目，分循環文法存在與否兩種情況討論：
該算法是深度優先的回溯搜索算法。一般情況下回溯算法的可終止性和正確性是能得到保證的。當它用于語言解析時，要防止由于循環文法(Cyclic Grammar)[21]引起推導無限循環，造成檢查無法終止。前述限制條件雖然沒有防止循環文法的出現，但是在算法中采取了措施保證跳出循環，從而使算法可終止，正確性也可得到保證。
定理1 給定滿足前述限制條件的體系結構風格屬性圖文法和體系結構屬性圖，驗證AAG對于ASGG是否約束滿足。算法1總可以保證驗證過程是可終止的。
證明 用|G|表示圖中元素數目，分循環文法存在與否兩種情況討論：
綜上所述，算法可終止性得證。
定理2 給定滿足前述限制條件的體系結構風格屬性圖文法和體系結構屬性圖，驗證AAG對于ASGG是否約束滿足。算法1總可以保證驗證結果是正確的。
綜上所述，算法的正確性得證。
算法還可以優化，如子圖匹配優化、分層規則、沖突對分析等[22]。該算法不但可用于檢查體系結構實例屬性圖是否遵循體系結構風格屬性圖文法，還可對某些非基于屬性圖文法描述的體系結構進行檢查。此時首先使用ASGG描述體系結構所遵循的體系結構風格，然后用AAG描述待檢查體系結構，最后用該算法來驗證。
2 Master/Slave結構例子
Master/Slave結構中，Master負載被分配給各Slave，其基本約束是：所有Slave總的計算能力必須不小于Master要分配的負載。下面用ASGGMS描述Master/Slave結構風格。假定Master負載和Slave計算能力都是自然數。
產生式p1表示在M/S結構中新增一個S標記節點。在產生式p1左部圖L中，1:M(w=v)表示節點1的標記是M，屬性w值為v；2:X表示節點2的標記為X。右部圖R中1:M(w=v-y)表示節點1標記為M，屬性w值為v-y；2:X表示節點2的標記為X；3:S(c=y)表示節點3標記為S，屬性c值為y。q：L→R是屬性圖態射(產生式中虛箭頭表示圖態射，自然數上代數同態顯而易見)。A(p)是應用條件，肯定否定應用條件均為空，代數表達式約束v>y表示節點1分配的負載大于新加入節點3提供的計算能力。產生式p2的含義與p1類似，它表示刪除非終結節點，并加入一個S標記節點。在這個產生式集合中，M/S結構的基本約束表達為：加入新的S標記節點，從M標記節點的負載中減去S標記節點提供的計算能力，最后不再加入S標記節點，M標記節點的負載值變為0，則得到的M/S結構圖滿足約束。
初始圖G0中1:M(w=v)表明M標記節點初始時要分配的負載為v，從初始圖出發，使用產生式進行推導，可以得到一系列的M/S結構實例屬性圖。圖4是從初始圖出發利用產生式序列p1p2推導得到M/S體系結構實例屬性圖的例子。在由初始圖進行推導時，首先要確定屬性w的值，在使用某個產生式時，要給出所加入的S標記節點的屬性c的值。在圖4中，為了討論方便，假定w=40，并且每次加入的S標記節點屬性c=20。
接下來定義規則集合R={r1，r2，r3}，M/S結構屬性圖基于此規則集進行演化。規則r2，r3分別與產生式p1，p2一樣。r1的定義如圖5所示，它表示M標記節點新增負載，為了能新增S標記節點承擔新增負載，引入X標記節點。其否定應用條件中否定約束是n，其含義是指體系結構圖中不能有已經出現X標記的節點，即X標記節點最多只能出現一次。
圖4（c）表示的M/S結構屬性圖中節點1的負載發生了變化，增加40。該體系結構實例屬性圖要進行模擬演化，表現為基于規則集R的屬性圖轉換，按照規則序列r1r2r3進行轉換(這個基于規則序列的轉換與圖4產生式推導的例子類似)，得到模擬執行后體系結構實例屬性圖AAG′，如圖6所示。正如前文所述，要對AAG′進行約束驗證以保證演化將是合法的，產生式p1，p2滿足規定的產生式限制條件，因此可使用前述約束檢查算法進行檢查，發現可以找到產生式序列p1p1p1p2。從初始圖G0(w=80)按此序列進行推導得到的圖與AAG′是屬性圖同構的。因此演化模擬執行后得到的體系結構屬性圖AAG′仍然遵循M/S結構風格，該演化合法，可被真正執行。
3 檢查器設計與實現
利用TU Berlin的屬性圖文法系統AGG的圖形解析器設計和實現了體系結構自動檢查器。AGG使用SPO的代數方法進行屬性圖轉換，有較強的圖形解析能力。該檢查器應用到了面向體系結構的服務集成開發平臺Artemis—ARC系統中，可對屬性圖描述的體系結構實例進行約束檢查，對其他描述方式的體系結構實例，將其轉換為屬性圖描述后，仍可進行檢查。
3.1 設計
使用屬性圖文法方法進行約束驗證時，首先要有屬性圖文法描述的體系結構風格作為驗證依據，然后將非屬性圖描述的體系結構轉換為屬性圖描述形式，最后進行約束驗證。因此這個自動檢查器主要由體系結構風格描述庫、體系結構描述轉換器、約束檢查器三部分組成，如圖7所示。體系結構風格描述庫中存儲預定義好的體系結構風格屬性圖文法描述；體系結構描述轉換器負責將待驗證體系結構圖轉換為屬性圖描述形式，約束檢查器對其進行檢查。
圖7 體系結構檢查器結構圖
3.2 改進與實現
提出AGG 圖形解析器的初衷是支持圖形規約檢查，因此其在推導檢查上存在缺陷。在使用形如p=(A→aA)的產生式進行推導時，可能會不停使用該產生式造成檢查無法終止，這時可對產生式的前提條件加以限制，但不是所有情況下該方法都有效。前文給出了產生式限制條件，要求規則右部元素不少于左部元素，被重復使用的產生式會不停增加圖形元素數，最終元素數目將超過待檢查圖元素數目。因此第二種方法是修改AGG的API，在檢查過程中加入元素數目檢查，在推導中檢查轉換圖元素數目是否超過待檢查圖形元素數目；如超過，則回溯，嘗試使用其他產生式進行推導。另外，改進了事件觸發機制，使檢查過程可以更詳細地顯示出來。在改進AGG的圖形解析器基礎上，實現了體系結構自動檢查器。
（1）體系結構風格描述庫：利用AGG提供的可視化編輯環境，預先編輯多種體系結構風格的屬性圖文法描述，這些體系結構風格描述以XML文件存放。要注意的是，AGG圖形解析器中規則的嘗試次序是根據XML文件中規則存放的順序進行的，因此在編輯圖文法時注意規則的編輯順序可以減少檢查過程回溯次數，在一定程度上提高檢查效率。
（2）體系結構描述轉換器：從體系結構風格描述庫中得到構件、連接器類型信息，將非屬性圖描述的體系結構轉換為AGG中屬性圖描述的形式。其基本思想是首先將運行時體系結構對象中構件、連接子轉換為AGG中的節點、邊，然后根據體系結構對象的拓撲信息構造得到體系結構實例屬性圖。在轉換過程中進行了初步檢查。如果無法完成從體系結構對象到屬性圖描述的轉換，即轉換時發現無法找到與構件(連接子)屬性Type值匹配的節點(邊)類型。此時檢查器即可判定該體系結構對象不屬于預定的體系結構風格，而無須進行下一步檢查。
（3）約束檢查器：調用改進的圖形解析器進行檢查，從體系結構描述轉換器中得到屬性圖描述的待檢查體系結構，從體系結構風格描述庫中載入體系結構風格圖文法描述和初始圖，根據這些判斷待檢查圖是否約束滿足。
3.3 效果
體系結構需動態演化時演化模擬執行，檢查器對模擬執行后的體系結構進行約束驗證，如演化合法，使動態演化真正付諸執行。圖8是對M/S結構模擬演化后進行約束驗證的例子。
三個體系結構是模擬演化后的體系結構，M，S是構件類型，D是連接子類型。圖8(a)中Comp1屬性值w=0時，檢查器將該體系結構轉換為圖4(c)屬性圖的形式，從初始圖按產生式序列p1p2推導，圖4(c)可達，演化合法；當w≠0時，不滿足M/S結構的基本約束，檢查器無法找到合適的產生式序列，演化非法。圖8(b)在進行體系結構描述轉換時，發現類型為S′的構件找不到匹配節點，檢查器報錯。圖8(c)中連接子Con1方向有錯，檢查器報錯。
4 結束語
討論了一種基于屬性圖文法的體系結構描述和約束驗證方法。首先使用屬性圖文法形式地描述了體系結構風格、體系結構實例和演化，給出約束滿足定義和約束檢查算法；然后以M/S結構為例說明如何基于屬性圖文法描述體系結構和進行約束驗證；最后設計和實現了基于AGG的圖形解析器體系結構檢查器，并將其應用到了Artemis—ARC系統中。這種基于屬性圖文法的體系結構描述和約束驗證方法直觀易理解，相對于文獻[11，13，14]的基于圖的描述和驗證方法，刻畫了體系結構的屬性信息，進行了包括屬性在內的約束驗證。
本文中體系結構演化首先被模擬執行，并對模擬執行后體系結構進行約束驗證；如滿足約束，則演化被真正付諸執行，該方法效率相對較低。體系結構的演化表現為體系結構實例屬性圖轉換，因此下一步工作是在體系結構實例屬性圖轉換過程中進行檢查，判斷每一步轉換是否會導致最后得到的體系結構實例屬性圖違反約束。該方法效率相對較高，并且可以在演化過程中盡早地判斷最后的結果是否會違反約束。
本文中所涉及到的圖表、注解、公式等內容請以PDF格式閱讀原文。
