基于情態(tài)演算的UML形式化驗(yàn)證與OCL約束自動(dòng)生成研究.pdf

1、從軟件工程中軟件生命周期的角度分析,軟件架構(gòu)是軟件的核心結(jié)構(gòu)與行為,因而軟件架構(gòu)的設(shè)計(jì)是軟件設(shè)計(jì)的核心,也是隨后進(jìn)行代碼開(kāi)發(fā)的基礎(chǔ)。因此軟件架構(gòu)設(shè)計(jì)的重要性不言而喻。由于軟件架構(gòu)設(shè)計(jì)本身是一種建?；顒?dòng),如何對(duì)軟件架構(gòu)設(shè)計(jì)的標(biāo)準(zhǔn)建模語(yǔ)言UML進(jìn)行正確性驗(yàn)證是一個(gè)難題。傳統(tǒng)軟件驗(yàn)證方法有著不夠精確、非自動(dòng)化等不足。另外,對(duì)UML進(jìn)行正確性驗(yàn)證需要得到UML的形式化語(yǔ)義,而UML本身是一種圖形化的表示方法,不具有形式化的語(yǔ)義。因此本文將采用形

2、式化方法來(lái)對(duì)UML模型進(jìn)行形式化描述,即為其賦予等價(jià)的形式化語(yǔ)義,再根據(jù)其語(yǔ)義進(jìn)行形式化驗(yàn)證。為了進(jìn)一步精確描述UML模型的語(yǔ)義,為其提供OCL約束是一種主流方法。而OCL約束需要人手工編寫(xiě),同樣具有正確性難以保證、人員開(kāi)銷等問(wèn)題,因此為UML模型自動(dòng)生成OCL約束模板是一種很好的解決方法,生成的OCL模板可供軟件設(shè)計(jì)人員參考,從而提高了軟件工程的整體效率。本文也將對(duì)OCL約束自動(dòng)生成進(jìn)行研究。
　　 UML是軟件設(shè)計(jì)過(guò)程事實(shí)上

3、的標(biāo)準(zhǔn)建模語(yǔ)言。本文首先從歷史發(fā)展、子圖種類、建模工具和以XMI表示的UML四個(gè)角度對(duì)UML作了簡(jiǎn)要的介紹,并具體介紹了即將研究的兩種UML子圖:類圖和狀態(tài)圖。同時(shí)介紹了形式化方法的基本概念和主要分支,并總結(jié)了國(guó)內(nèi)外現(xiàn)有的對(duì)UML形式化的研究。最后介紹了UML的標(biāo)準(zhǔn)子語(yǔ)言O(shè)CL、采用的形式化語(yǔ)言情態(tài)演算和它的具體實(shí)現(xiàn)--邏輯編程語(yǔ)言Prolog,并進(jìn)一步分析了從UML轉(zhuǎn)換到情態(tài)演算的可行性,從理論上確定了給出的解決方案的正確性。

4、　　 本文隨后給出了基于情態(tài)演算的UML形式化描述方法。首先分析了選擇UML類圖和狀態(tài)圖作為研究對(duì)象的意義,再分別對(duì)UML類圖和狀態(tài)圖進(jìn)行形式化描述:先是給出了兩種子圖的一種形式化語(yǔ)義結(jié)構(gòu);再分析了兩種子圖元素與數(shù)理邏輯和情態(tài)演算元素的對(duì)應(yīng)關(guān)系;又提出了兩種子圖到數(shù)理邏輯語(yǔ)句和Prolog代碼的轉(zhuǎn)換算法,并以偽代碼的形式給出。然后著重定義了UML模型的兩種基本錯(cuò)誤類型:領(lǐng)域無(wú)關(guān)的UML模型語(yǔ)法錯(cuò)誤和領(lǐng)域相關(guān)的UML模型語(yǔ)義錯(cuò)誤,并給出

5、具體錯(cuò)誤實(shí)例和自動(dòng)生成的Prolog代碼。
　　 進(jìn)一步,本文討論了如何實(shí)現(xiàn)對(duì)UML模型的OCL約束模板自動(dòng)生成。首先強(qiáng)調(diào)了OCL約束自動(dòng)生成的研究意義,同時(shí)給出了OCL約束的應(yīng)用范圍。從而進(jìn)一步分析了如何在UML模型中提取OCL約束的目標(biāo)應(yīng)用對(duì)象,并給出了一種提取算法。最后給出了該提取算法的Perl示例代碼的具體實(shí)現(xiàn)。
　　 作為上述理論的補(bǔ)充和可行性證明,后續(xù)章節(jié)詳細(xì)介紹了以UML子圖到情態(tài)演算的轉(zhuǎn)換算法和OCL約束

6、模板自動(dòng)生成算法為基礎(chǔ)而設(shè)計(jì)并實(shí)現(xiàn)的UML形式化驗(yàn)證原型工具USCVSC。首先建立了該原型工具的系統(tǒng)實(shí)現(xiàn)框架和代碼框架。其次給出了該原型工具的用戶界面,并詳細(xì)描述了其中的4個(gè)基本子功能界面。最后說(shuō)明了,通過(guò)此原型工具,可以實(shí)現(xiàn)UML模型語(yǔ)法檢查和語(yǔ)義錯(cuò)誤驗(yàn)證,以及OCL約束模板自動(dòng)生成的綜合性功能。
　　 最后,本文對(duì)USCVSC原型工具的使用進(jìn)行了介紹,并結(jié)合一個(gè)大學(xué)教學(xué)系統(tǒng)和大學(xué)申請(qǐng)系統(tǒng)的實(shí)際案例來(lái)對(duì)原型工具的基本功能進(jìn)行演

7、示。先描述了該應(yīng)用實(shí)例的特點(diǎn),并用UML建模工具對(duì)其類圖和狀態(tài)圖進(jìn)行設(shè)計(jì)。接下來(lái)則利用USCVSC原型工具對(duì)預(yù)定義的UML模型錯(cuò)誤進(jìn)行驗(yàn)證:對(duì)于UML語(yǔ)法錯(cuò)誤的檢查可以在USCVSC原型工具中完成,對(duì)于UML語(yǔ)義錯(cuò)誤的驗(yàn)證則需要USCVSC原型工具和Prolog解析器一起協(xié)同完成。最后演示了如何利用USCVSC原型工具為UML類圖自動(dòng)生成OCL約束模板,并給出了示例OCL約束語(yǔ)句。
　　 綜上所述,本文以形式化語(yǔ)言情態(tài)演算為描述