面向?qū)ο蟮能浖?guī)格說明的構(gòu)造及確認(rèn)技術(shù)研究.pdf

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

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

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

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

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

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