UML模型圖到B方法形式規(guī)約的轉(zhuǎn)換研究與應(yīng)用.pdf

1、形式化方法(Formal Method)基于嚴(yán)格的數(shù)學(xué)理論，能產(chǎn)生精確、無(wú)二義性的形式規(guī)約，為軟件開發(fā)提供了嚴(yán)格的數(shù)學(xué)基礎(chǔ)，對(duì)提高軟件的可靠性有著非常顯著的作用。形式化方法要求開發(fā)者具有良好的數(shù)學(xué)基礎(chǔ)，并使用嚴(yán)格的數(shù)學(xué)符號(hào)去編寫規(guī)約，這使得很多軟件開發(fā)者難以接受。同時(shí)，形式規(guī)約不夠直觀，可讀性較差，不便于與用戶進(jìn)行交流。因此，形式化方法的研究和應(yīng)用仍然局限在較小的范圍之內(nèi)。 UML 是一種可視化的圖形建模語(yǔ)言，采用直觀的圖形表示

2、法為系統(tǒng)進(jìn)行建模，能得到圖形化的軟件規(guī)約，已在面向?qū)ο蠓治龊驮O(shè)計(jì)中成為事實(shí)上的工業(yè)標(biāo)準(zhǔn)。但是，UML 的許多概念都基于非形式化語(yǔ)義，對(duì)模型的描述不夠準(zhǔn)確，容易產(chǎn)生模糊或歧義，缺乏精確的語(yǔ)義，不便于使用工具對(duì)其描述的規(guī)約進(jìn)行動(dòng)態(tài)分析和驗(yàn)證。 形式化方法和 UML 存在很大的互補(bǔ)性，形式化方法恰好能在精確語(yǔ)義方面彌補(bǔ) UML 的不足，能夠?qū)?UML 建模結(jié)果進(jìn)行一致性檢查和正確性分析。同時(shí)，UML 可以降低直接使用形式化方法的難度，

3、增加形式化方法在軟件開發(fā)中的實(shí)際作用。二者的結(jié)合研究將對(duì)提高軟件的可靠性有著非常重要的意義。 在分析UML模型圖特點(diǎn)的基礎(chǔ)上，本文選擇B方法作為UML模型圖的形式規(guī)約方法，_是因?yàn)锽方法具有面向?qū)ο蟮念愃铺卣鳎梢允筓ML模型圖到B方法形式規(guī)約的轉(zhuǎn)換過(guò)程直觀易懂；二是因?yàn)锽方法有一整套嚴(yán)格的理論分析方法和工具，彌補(bǔ)了UML模型圖缺乏驗(yàn)證工具的不足；三是因?yàn)锽方法支持軟件開發(fā)的幾乎全過(guò)程，包括規(guī)約、精化、代碼生成、正確性驗(yàn)證等。

4、 本文中，我們主要針對(duì)UML模型圖的類圖和狀態(tài)圖，分別給出二者到B方法形式規(guī)約的轉(zhuǎn)換方法。軟件開發(fā)人員可以首先結(jié)合UML類圖和狀態(tài)圖對(duì)目標(biāo)系統(tǒng)進(jìn)行建模，然后根據(jù)文中所給出的轉(zhuǎn)換方法，構(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)。 最后，結(jié)合了一個(gè)電梯實(shí)例，說(shuō)明了UML模型圖到B方法形式規(guī)約的轉(zhuǎn)換方法及過(guò)程，并在B方