UML模型與形式模型雙向轉(zhuǎn)換的研究.pdf

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

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

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