[發(fā)明專利]一種從EGG圖文法到RGG圖文法的轉換方法

無效

• 申請?zhí)枺?/td>: 201210443734.8
• 申請日: 2012-11-08
• 公開（公告）號: CN102929639A
• 公開（公告）日: 2013-02-13
• 發(fā)明（設計）人: 鄒陽;曾曉勤
• 申請（專利權）人: 河海大學
• 主分類號: G06F9/44
• 分類號: G06F9/44
• 代理公司: 南京蘇高專利商標事務所(普通合伙) 32204
• 代理人: 夏雪

技術領域

本發(fā)明屬于計算機數(shù)據(jù)處理技術領域，涉及一種軟件形式化建模、分析與驗證的方法，具體是一種從EGG圖文法到RGG圖文法的轉換方法。

背景技術

圖文法是對圖進行定義和語法結構分析的形式化方法。近年來，圖文法已廣泛應用于可視化語言領域，是軟件系統(tǒng)形式化建模、描述、分析、轉換和驗證的形式化工具。圖文法主要包括上下文相關和上下文無關兩大類，每一類圖文法又包含若干個形式框架。一個圖文法形式框架一般由圖產(chǎn)生式的形式定義、圖柄定義、嵌入規(guī)則與子圖替換方法和所生成圖語言的形式定義，以及一個與之對應的規(guī)約算法組成。而一個圖文法形式框架的圖文法實例則由一個初始圖和一組具體的圖產(chǎn)生式構成，其中，一個圖產(chǎn)生式由一對(稱為左圖和右圖)滿足一定約束的圖構成。EGG(Edged?Graph?Grammar)和RGG(Reserved?Graph?Grammar)是目前應用較為廣泛的上下文相關圖文法的形式框架。

在軟件形式化建模、分析與驗證過程中，圖文法形式框架的一般應用途徑為：依據(jù)該形式框架的產(chǎn)生式形式設計具體的圖產(chǎn)生式集合(也就是圖文法實例)來描述應用中所涉及的圖形式的結構，再應用該框架配備的規(guī)約算法對所關注的圖進行分析以驗證相關的結構特性。如此一來，同屬上下文相關圖文法的不同圖文法形式框架在實際應用中被完全隔離開來：一旦選擇了某種圖文法形式框架去描述軟件工程領域中的一個具體應用，就只能選擇此形式框架所配備的規(guī)約算法進行相應的分析與驗證。

然而，上述兩種形式框架在圖的描述和分析功能上各有利弊。EGG圖文法產(chǎn)生式的形式非常簡潔，也比較直觀，因而便于用戶設計圖產(chǎn)生式來描述應用中的所涉及圖結構；但其規(guī)約算法較為復雜，算法時間復雜度為指數(shù)級，分析效率較為低下，使其難以應用于復雜系統(tǒng)的建模與分析。而RGG圖文法由于引入了雙層結點結構和頂點標記機制，產(chǎn)生式的形式較為復雜，難于理解，給實際應用中設計圖產(chǎn)生式的用戶帶來諸多的困難；但其規(guī)約算法在滿足合流條件情形下的時間復雜度僅為多項式級，算法分析效率很高。然而，在針對某個具體應用選擇上下文相關圖文法工具時用戶只能局限于一種形式框架，而不能分別在描述與分析時揚長避短地選擇合適的形式框架，因而一方面導致了上述兩種圖文法形式框架在實際應用中難于凸顯自身的優(yōu)勢，另一方面也限制了他們各自的應用范圍。

發(fā)明內容

發(fā)明目的：針對上述現(xiàn)有技術存在的問題和不足，本發(fā)明的目的是提供一種從EGG圖文法到RGG圖文法的轉換方法，使這兩種圖文法形式框架緊密關聯(lián)起來形成一個綜合的形式化工具，以解決在實際應用中EGG和RGG相互獨立、因受限于各自缺點而難于充分發(fā)揮各自優(yōu)勢的問題。

技術方案：本發(fā)明構造了一種從EGG圖文法到RGG圖文法的轉換方法，主要包含以下步驟：一、將EGG圖文法實例轉換成對應的VRGG實例；二、將VRGG實例轉換成對應的RGG實例。

為方便理解，先簡要介紹EGG和RGG形式框架。EGG圖產(chǎn)生式是一對懸邊圖(通過在有向圖的部分結點上添加一條或多條帶有標號的懸邊，即不與該圖中的任何其他結點相連的邊，所形成的圖)，左圖和右圖上的標記懸邊是一一對應的；其圖柄是通過引入從產(chǎn)生式左、右圖的核圖(即刪除懸邊之后得到的有向圖)到主圖的同構映射來定義的。而RGG則引入了一種兩層結構結點：一個結點包含若干個頂點，結點本身則是一個超頂點，而頂點就是邊的連接點；以及頂點上的一種標記機制。一個RGG圖產(chǎn)生式是一對兩層結構結點所構成的圖，圖中的上下文頂點被標記，且滿足左、右圖中的被標記頂點一一對應、標記相同。RGG的圖柄定義是通過從產(chǎn)生式左、右圖到主圖的同構映射來建立的。

可見，EGG和RGG在產(chǎn)生式的形式上區(qū)別較大，為了彌合這一差異，引入了一種中間圖文法形式框架VRGG。VRGG與RGG的不同之處僅在于它對RGG中頂點所連接邊的數(shù)目作了限制：在圖柄匹配時，對于產(chǎn)生式中任何標記頂點v，主圖中與頂點v的象(同構映射下)相連的邊必須唯一；它與EGG的不同之處在于產(chǎn)生式的形式上的差異。

由于VRGG和RGG的圖產(chǎn)生式的形式完全相同，故上述步驟二只需將VRGG圖文法實例的圖柄定義改為RGG的圖柄定義即可，而無需改變產(chǎn)生式形式；而步驟一只涉及產(chǎn)生式形式的轉換，無需改變圖柄定義。