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

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

0 引言

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

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

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

1 UML建模和B方法介紹

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

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

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