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

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

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

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

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

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

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

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