摘要：统一建模语言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格式阅读原文”