ＵＭＬ模型到Ｂ抽象機的轉換和實現

摘要：統一建模語言UML廣泛用于面向對象技術的建模，B方法主要是用抽象機來描述軟件系統的規格說明。文章針對軟件開發中經常用到的UML模型，提出了基于B語言的UML形式化方法：通過將UML模型轉化為B抽象機，實現了UML模型的形式化。實例分析表明，轉換是可行的。

關鍵詞：UML；形式化方法；抽象機；B方法

0 引言

形式化方法以嚴密的數學為基礎，可以對系統進行嚴格、精確的規范，并可以對系統性質進行正確性驗證，最大限度地保證所開發系統性能的正確和可靠，因此在與安全有關的系統開發中越來越受重視。UML是一種面向對象的可視化的標準建模語言，它的特點是直觀，強調從整體上把握系統的結構和行為特性；但UML的許多概念基于非形式化語義，對模型的描述不精確，不便用工具對其所描述的需求進行驗證。顯然，UML與形式化方法是互補的，二者的結合將對高可信軟件工程產生重要影響，因此成為近年來的研究熱點。

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

根據UML和B方法的特點，本文針對一個電梯系統構建UML模型，由于UML本身不能提供對模型的精確性證明，此時再用B方法對安全性要求高的模型建立抽象機規范，進行精確性證明，從而保證模型的正確性，實現UML的形式化。此時還可對建立的抽象機規范進一步實施精化，建立更接近實現的模型。

1 UML建模和B方法介紹

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

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

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