随着信息技术的飞速发展,计算机软件系统的应用逐渐扩展到了社会的各个领域。软件规模和复杂度在不断增加,软件出现错误的可能性也随之增加。如何保证软件的质量、提高软件的可靠性,已成为目前软件工程研究领域的一个热点。将形式化方法和主流的软件开发方法相结合是一种可行的方法。UML作为当前比较流行的一种可视化建模语言,已成为面向对象分析和设计中事实上的工业标准。UML模型直观、易懂,利于开发者与用户之间的沟通。但UML的大部分语义是用自然语言描述的,确乏精确的语义,容易产生模糊或歧义;UML缺乏有效的推理机制和完善的模型检查能力,不便于使用工具对其描述的规约进行动态分析和验证。形式化方法则是基于严格数学理论的,能产生精确、无二义性的形式规约,为软件开发提供了严格的数学基础,这对提高软件的可靠性有着非常显著的作用。但形式规约不够直观,可读性较差,不便于与用户进行交流,要求开发者具有良好的数学基础。因此,形式化方法的研究和应用目前仍局限在较小的范围之内。把形式化方法和UML相结合实现优势互补的研究对保证软件质量、提高可靠性有着非常重要的意义。本文选择B方法作为形式规约方法,把UML模型的图形规约映射到B形式规约。一方面,我们能够借助于强大的B方法支持工具,基于相应的B形式规约,对UML建模结果进行正确性分析和一致性检查;另一方面,可将UML规约作为形式化开发的基础,降低直接使用B方法建立形式规约的难度,增强B方法在软件开发中的实际作用。本文以UML用例模型为主要研究对象,在分析UML用例模型概念和B抽象机符号的基础上,对用例模型建模元素的抽象语法进行描述,建立两者之间的映射,实现UML用例模型图到B形式规约的转换。软件开发人员可以首先用半形式化的UML用例模型为目标系统建立需求模型,然后根据文中给出方法构建目标系统的B形式化规约,再利用B方法支持工具对规约进行动态分析和模型验证,得出可靠的形式规约,为在此基础上进行的形式推导和精化提供了正确的起点。最后,通过对电梯控制系统的实例分析,进一步详述了UML用例模型到B方法形式规约的转换方法及过程,并利用B方法的支持工具ProB对所得到的形式化模型进行了动态分析和模型检测。