1、隨著計算機硬件性能迅速提高和價格的持續(xù)下降，計算機系統(tǒng)應用范圍不斷地擴大，軟件系統(tǒng)也日益復雜，研究如何提高軟件質量和軟件開發(fā)效率的工作變得日益重要。 UML語言已成為軟件工程領域事實上的標準建模語言，它提供了豐富的建模機制，并且容易讓用戶理解，因此在抽取和定義用戶需求階段獲得了廣泛的應用。但由于UML語言缺乏精確的語義，而使得分析設計人員難以建立精確的需求模型，更難以使用工具對模型自動進行系統(tǒng)的分析和驗證。 形式方法則是

2、一種基于數(shù)學的軟件開發(fā)方法，形式方法能對系統(tǒng)應該滿足的性質進行描述，它具有精確性，一致性和無歧義性等特點，并且能夠對規(guī)格說明進行分析和驗證，因此被認為是提高軟件質量的有效方法。然而，在工業(yè)界，形式方法大都僅用于安全攸關領域。形式方法被批評為難以使用，費時費力，由于需要分析設計人員具備良好的數(shù)學基礎和抽象思維能力，因此構建形式規(guī)格說明比較困難，并且缺少有效的和完整的工具來支持軟件開發(fā)人員使用形式方法。 在軟件的開發(fā)過程中怎樣才能有

3、效地結合面向對象方法與形式方法則是一個值得研究的課題，本文所做的工作和取得的成果主要體現(xiàn)在以下幾個方面： ●本文以UML和Object-z作為建模工具，提出了一種在軟件需求階段結合圖形化規(guī)格說明和形式方法，以獲得精確的軟件需求規(guī)格說明的方法。本文從整個系統(tǒng)的角度研究了如何實現(xiàn)從用戶需求得到圖形化規(guī)格說明，再到形式規(guī)格說明，并對規(guī)格說明進行有效確認的方法和技術。 ●在對圖形化規(guī)格說明技術與形式方法進行對比分析的基礎上，指出

4、了它們的優(yōu)缺點。通過分析得出了這樣的結論：將圖形化規(guī)格說明與形式方法結合，就能互相彌補雙方的缺陷和不足，并能最大限度地發(fā)揮出各自的優(yōu)勢。同時本文提出了一種結合圖形化方法與形式化方法來構造軟件需求規(guī)格說明的過程。 ●在UML與形式方法的結合過程中發(fā)揮了補充法和結合法的綜合優(yōu)勢，首先根據(jù)補充法的原則使用OCL對模型信息進行較為精確的描述，再使用結合法，即通過將帶OCL約束信息的UML模型轉換為Object-z規(guī)格說明使UML模型形式

5、化。使用Object-z就可以方便地表達面向對象的概念。在總結現(xiàn)有研究成果的基礎上，通過分析現(xiàn)有研究成果中的不足之處，系統(tǒng)地提出了一整套從UML類圖，狀態(tài)圖以及用例圖到Object-Z規(guī)格說明的轉換規(guī)則，并用一個電梯系統(tǒng)的實例加以說明。 ●在結合UML與Object-Z的研究過程中，發(fā)現(xiàn)OCL語言與Object-Z語言具有很強的互補性，給出了從OCL表達式系統(tǒng)地轉換到Object-z規(guī)格說明的方法。本方法結合了UML/OCL模型

6、直觀性與Object-Z語言的嚴密性優(yōu)點，可產生更為完全的Object-Z規(guī)格說明。為了支持本文提出的方法，又開發(fā)了基于XMI的工具UMLFormalizer，初步實現(xiàn)了從UML模型到Object-Z的自動轉換。 ●目前常見Object-Z存儲交換格式有基于Latex和基于XML格式兩種，本文在對這兩種常見存儲交換格式進行分析比較的基礎上，認為采用XML格式的Object-z規(guī)格說明文件更有利于形式開發(fā)工具的集成，并且對現(xiàn)有的O