UML用例模型的B形式化描述方法研究.pdf

1、隨著信息技術(shù)的飛速發(fā)展，計(jì)算機(jī)軟件系統(tǒng)的應(yīng)用逐漸擴(kuò)展到了社會(huì)的各個(gè)領(lǐng)域。軟件規(guī)模和復(fù)雜度在不斷增加，軟件出現(xiàn)錯(cuò)誤的可能性也隨之增加。如何保證軟件的質(zhì)量、提高軟件的可靠性，已成為目前軟件工程研究領(lǐng)域的一個(gè)熱點(diǎn)。將形式化方法和主流的軟件開發(fā)方法相結(jié)合是一種可行的方法。 UML作為當(dāng)前比較流行的一種可視化建模語言，已成為面向?qū)ο蠓治龊驮O(shè)計(jì)中事實(shí)上的工業(yè)標(biāo)準(zhǔn)。UML模型直觀、易懂，利于開發(fā)者與用戶之間的溝通。但UML的大部分語義是用自然

2、語言描述的，確乏精確的語義，容易產(chǎn)生模糊或歧義；UML缺乏有效的推理機(jī)制和完善的模型檢查能力，不便于使用工具對(duì)其描述的規(guī)約進(jìn)行動(dòng)態(tài)分析和驗(yàn)證。形式化方法則是基于嚴(yán)格數(shù)學(xué)理論的，能產(chǎn)生精確、無二義性的形式規(guī)約，為軟件開發(fā)提供了嚴(yán)格的數(shù)學(xué)基礎(chǔ)，這對(duì)提高軟件的可靠性有著非常顯著的作用。但形式規(guī)約不夠直觀，可讀性較差，不便于與用戶進(jìn)行交流，要求開發(fā)者具有良好的數(shù)學(xué)基礎(chǔ)。因此，形式化方法的研究和應(yīng)用目前仍局限在較小的范圍之內(nèi)。把形式化方法和UML

3、相結(jié)合實(shí)現(xiàn)優(yōu)勢(shì)互補(bǔ)的研究對(duì)保證軟件質(zhì)量、提高可靠性有著非常重要的意義。 本文選擇B方法作為形式規(guī)約方法，把UML模型的圖形規(guī)約映射到B形式規(guī)約。一方面，我們能夠借助于強(qiáng)大的B方法支持工具，基于相應(yīng)的B形式規(guī)約，對(duì)UML建模結(jié)果進(jìn)行正確性分析和一致性檢查；另一方面，可將UML規(guī)約作為形式化開發(fā)的基礎(chǔ)，降低直接使用B方法建立形式規(guī)約的難度，增強(qiáng)B方法在軟件開發(fā)中的實(shí)際作用。 本文以UML用例模型為主要研究對(duì)象，在分析UML用

4、例模型概念和B抽象機(jī)符號(hào)的基礎(chǔ)上，對(duì)用例模型建模元素的抽象語法進(jìn)行描述，建立兩者之間的映射，實(shí)現(xiàn)UML用例模型圖到B形式規(guī)約的轉(zhuǎn)換。軟件開發(fā)人員可以首先用半形式化的UML用例模型為目標(biāo)系統(tǒng)建立需求模型，然后根據(jù)文中給出方法構(gòu)建目標(biāo)系統(tǒng)的B形式化規(guī)約，再利用B方法支持工具對(duì)規(guī)約進(jìn)行動(dòng)態(tài)分析和模型驗(yàn)證，得出可靠的形式規(guī)約，為在此基礎(chǔ)上進(jìn)行的形式推導(dǎo)和精化提供了正確的起點(diǎn)。最后，通過對(duì)電梯控制系統(tǒng)的實(shí)例分析，進(jìn)一步詳述了UML用例模型到B方法