基于UML類圖的B形式化規(guī)約研究.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)。本文將UML與B方法相結(jié)合進(jìn)行研究，試圖克服形式化開(kāi)發(fā)方法在需求規(guī)約描述方面的不足。
　　 本文首先分別對(duì)UML和B方法進(jìn)行分析研究，半形式化的UML缺乏精確的語(yǔ)義，容易產(chǎn)生模糊和歧義，而B(niǎo)方法則基于嚴(yán)格的數(shù)

2、學(xué)理論，能產(chǎn)生精確、無(wú)二義的形式規(guī)約，為軟件開(kāi)發(fā)提供了嚴(yán)格的數(shù)學(xué)基礎(chǔ)。其次選取UML靜態(tài)模型中類圖為主要研究對(duì)象，對(duì)類圖建模元素的抽象語(yǔ)法進(jìn)行分析；采用B方法形式規(guī)約語(yǔ)言對(duì)UML類圖建模元素進(jìn)行形式化描述，進(jìn)一步刻畫(huà)其語(yǔ)義，建立類圖建模元素與B方法符號(hào)記法之間的形式化映射規(guī)則，實(shí)現(xiàn)UML類圖到B方法形式規(guī)約的轉(zhuǎn)換。最后通過(guò)電梯控制系統(tǒng)實(shí)例說(shuō)明UML類圖到B方法形式規(guī)約的轉(zhuǎn)換方法及其應(yīng)用過(guò)程，并應(yīng)用B方法的支持工具ProB對(duì)所得到的形式化