ＵＭＬ模型到Ｂ抽象機(jī)的轉(zhuǎn)換和實(shí)現(xiàn)

摘要：統(tǒng)一建模語言UML廣泛用于面向?qū)ο蠹夹g(shù)的建模，B方法主要是用抽象機(jī)來描述軟件系統(tǒng)的規(guī)格說明。文章針對軟件開發(fā)中經(jīng)常用到的UML模型，提出了基于B語言的UML形式化方法：通過將UML模型轉(zhuǎn)化為B抽象機(jī)，實(shí)現(xiàn)了UML模型的形式化。實(shí)例分析表明，轉(zhuǎn)換是可行的。

關(guān)鍵詞：UML；形式化方法；抽象機(jī)；B方法

0 引言

形式化方法以嚴(yán)密的數(shù)學(xué)為基礎(chǔ)，可以對系統(tǒng)進(jìn)行嚴(yán)格、精確的規(guī)范，并可以對系統(tǒng)性質(zhì)進(jìn)行正確性驗證，最大限度地保證所開發(fā)系統(tǒng)性能的正確和可靠，因此在與安全有關(guān)的系統(tǒng)開發(fā)中越來越受重視。UML是一種面向?qū)ο蟮目梢暬臉?biāo)準(zhǔn)建模語言，它的特點(diǎn)是直觀，強(qiáng)調(diào)從整體上把握系統(tǒng)的結(jié)構(gòu)和行為特性；但UML的許多概念基于非形式化語義，對模型的描述不精確，不便用工具對其所描述的需求進(jìn)行驗證。顯然，UML與形式化方法是互補(bǔ)的，二者的結(jié)合將對高可信軟件工程產(chǎn)生重要影響，因此成為近年來的研究熱點(diǎn)。

B方法是一種基于自動定理證明的形式化方法，支持軟件開發(fā)的全過程，它有完整的工具支持：B-Toolkit和Atelier-B，已經(jīng)在高可信軟件實(shí)踐中得到成功應(yīng)用，因此將UML與B方法集成被認(rèn)為是很有前途的。

根據(jù)UML和B方法的特點(diǎn)，本文針對一個電梯系統(tǒng)構(gòu)建UML模型，由于UML本身不能提供對模型的精確性證明，此時再用B方法對安全性要求高的模型建立抽象機(jī)規(guī)范，進(jìn)行精確性證明，從而保證模型的正確性，實(shí)現(xiàn)UML的形式化。此時還可對建立的抽象機(jī)規(guī)范進(jìn)一步實(shí)施精化，建立更接近實(shí)現(xiàn)的模型。

1 UML建模和B方法介紹

UML定義了9種不同的圖。9種圖分為兩類，一類是靜態(tài)圖，包括用例圖、類圖、對象圖、組件圖和配置圖；另一類是動態(tài)圖，包括序列圖、協(xié)作圖、狀態(tài)圖和活動圖。其中用例圖、活動圖和交互圖是UML極具特色的部分。這9種圖從不同應(yīng)用層次和不同角度為軟件系統(tǒng)從系統(tǒng)分析、設(shè)計直至實(shí)現(xiàn)提供了有力支持，使用這些圖可以描繪任何復(fù)雜的系統(tǒng)。

B方法是一種面向模型的數(shù)學(xué)方法，它在軟件開發(fā)的各個階段采用統(tǒng)一的AMN(Abstract Machine Notation)符號語言描述系統(tǒng)規(guī)約及系統(tǒng)設(shè)計，用內(nèi)嵌的邏輯符號、基本集合符號、關(guān)系符號以及數(shù)學(xué)對象符號來描述系統(tǒng)的靜態(tài)結(jié)構(gòu)，用廣義代換語言GSL描述系統(tǒng)的動態(tài)行為。在B方法中，軟件系統(tǒng)被模型化為一個由多個相互依存的抽象機(jī)所組成的集合，稱為B模型。B模型由3種類型的B組件共同表達(dá)：抽象機(jī)(MA-CHINE)，精化(REFINEMENT)和實(shí)現(xiàn)(IMPLEMENTATION)。在B方法中，軟件開發(fā)的過程就是一個對模型規(guī)約(抽象機(jī)集合)逐步精化直至實(shí)現(xiàn)的過程。B抽象機(jī)的定義如下：

注：“本文中所涉及到的圖表、注解、公式等內(nèi)容請以PDF格式閱讀原文”