形式化方法(Formal Method)基于严格的数学理论,能产生精确、无二义性的形式规约,为软件开发提供了严格的数学基础,对提高软件的可靠性有着非常显著的作用。形式化方法要求开发者具有良好的数学基础,并使用严格的数学符号去编写规约,这使得很多软件开发者难以接受。同时,形式规约不够直观,可读性较差,不便于与用户进行交流。因此,形式化方法的研究和应用仍然局限在较小的范围之内。UML是一种可视化的图形建模语言,采用直观的图形表示法为系统进行建模,能得到图形化的软件规约,已在面向对象分析和设计中成为事实上的工业标准。但是,UML的许多概念都基于非形式化语义,对模型的描述不够准确,容易产生模糊或歧义,缺乏精确的语义,不便于使用工具对其描述的规约进行动态分析和验证。形式化方法和UML存在很大的互补性,形式化方法恰好能在精确语义方面弥补UML的不足,能够对UML建模结果进行一致性检查和正确性分析。同时,UML可以降低直接使用形式化方法的难度,增加形式化方法在软件开发中的实际作用。二者的结合研究将对提高软件的可靠性有着非常重要的意义。在分析UML模型图特点的基础上,本文选择B方法作为UML模型图的形式规约方法,一是因为B方法具有面向对象的类似特征,可以使UML模型图到B方法形式规约的转换过程直观易懂;二是因为B方法有一整套严格的理论分析方法和工具,弥补了UML模型图缺乏验证工具的不足;三是因为B方法支持软件开发的几乎全过程,包括规约、精化、代码生成、正确性验证等。本文中,我们主要针对UML模型图的类图和状态图,分别给出二者到B方法形式规约的转换方法。软件开发人员可以首先结合UML类图和状态图对目标系统进行建模,然后根据文中所给出的转换方法,构建目标系统的B方法形式规约,再利用B方法支持工具对规约进行动态分析和验证,得出可靠的形式规约,并为在此基础上进行的形式推导和精化提供了正确的起点。最后,结合了一个电梯实例,说明了UML模型图到B方法形式规约的转换方法及过程,并在B方法支持工具(ProB)中对所得到的形式化模型进行了动态分析和模型检测。