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

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

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

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

4、 本文中，我們主要針對UML模型圖的類圖和狀態(tài)圖，分別給出二者到B方法形式規(guī)約的轉(zhuǎn)換方法。軟件開發(fā)人員可以首先結(jié)合UML類圖和狀態(tài)圖對目標系統(tǒng)進行建模，然后根據(jù)文中所給出的轉(zhuǎn)換方法，構建目標系統(tǒng)的 B 方法形式規(guī)約，再利用 B 方法支持工具對規(guī)約進行動態(tài)分析和驗證，得出可靠的形式規(guī)約，并為在此基礎上進行的形式推導和精化提供了正確的起點。 最后，結(jié)合了一個電梯實例，說明了UML模型圖到B方法形式規(guī)約的轉(zhuǎn)換方法及過程，并在B方