UML模型與形式模型雙向轉換的研究.pdf

1、UML提供了圖形概念來表示面向對象軟件系統(tǒng)的設計。在軟件設計領域，它已經(jīng)成為了事實上的工業(yè)標準。然而UML缺乏精確語義且是一種半形式化語言。形式化規(guī)格語言試圖為軟件開發(fā)提供一種精確的、完備規(guī)格說明方法。許多研究者做了許多研究工作來把UML模型轉換到形式模型以分析和驗證UML模型。但是由于很難證明形式描述和非形式描述之間的等價性，因此需要在兩個領域之間進行不斷的來回往復。因此需要形式模型逆向轉換回到UML模型。
　　 Z語言易于描

2、述軟件系統(tǒng)的靜態(tài)結構，因此本文首先利用UMLTranZ的方法實現(xiàn)了UML模型到形式模型的轉換。UMLTranZ方法能夠將UML概念類圖轉換到Z模型。Z模型的主要架構是Schema，它能夠形式的描述UML概念類圖的語義。利用現(xiàn)存的形式模型分析工具可以對Z模型進行分析推理和證明。
　　 XMI(XML Metamodel Interchange)是由OMG提供的模型交換數(shù)據(jù)格式。利用XMI提供的傳送模型不同部分的機制，我們提出了一種

3、形式模型逆向轉換UML模型的轉換方法。這種逆向轉換方法是一種間接的逆向轉換方法，它能夠在最大程度上減少UML模型轉換到形式模型過程中所產(chǎn)生的弱化影響。將這種逆向轉換方法與現(xiàn)有正向的轉換方法向結合就能成功的實現(xiàn)UML模型和形式模型之間的雙向轉換。
　　 我們還利用了UTP理論形式的證明了逆向轉轉換方法的正確性和可行性。對應于通過UMLTranZ所得到的Z模型，我們基于一階邏輯謂詞和集合論定義了Z模型到UML概念類圖的逆向轉換具體映