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

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

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

0 引言

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

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

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