统一建模语言(UML)是目前比较成熟的建模语言,运用非常广泛。UML支持面向对象的分析与设计,提供了一批基本的表示模型元素的图形和方法,能简洁明了地表达面向对象的各种概念和模型元素,用于对软件进行描述、可视化处理、构造和建立软件系统制品的文档等。作为一种图形化语言,UML模型图形能清晰地表示系统的逻辑模型或实现模型,其强大表达能力使它可以用于各种复杂类型的软件系统的建模。但是,UML也存在缺乏精确的语义、不够精练、存在二义性及结果的正确性难以验证等问题。形式化方法是建立在严格数学基础上的软件开发方法,能够精确地、无二义地描述系统,并且有严格的证明。B方法是一种较为实用的形式化软件开发方法,覆盖了从抽象规约到可执行代码生成的过程,拥有强有力的支持工具。B方法使用抽象机符号(AMN)来构造模型,并支持规范说明的类型检测和动态验证。B方法的支持工具可用动画等方式模拟运行规范说明,根据需求和测试场景检查获得的规范说明是否符合需求,对提高软件的可靠性有着非常显著的作用。UML与B方法的有机结合,既保留了UML在建模方面的优势,又弥补了UML的不足。B方法为UML模型提供精确的语义参考,有助于消除UML模型的歧义、模型内部及模型之间的不一致性。同时,直观易懂的UML模型图降低了直接使用B方法的难度,加强了形式规约的可理解性和可维护性。二者的有机结合提高了软件开发的精确性和效率。本文首先分析了B方法的数学基础和抽象机理论,简单介绍了UML语言,在此基础上,分别给出了UML的类图和状态图的B方法的形式化描述。软件开发过程中,首先结合UML类图和状态图对目标系统建模,再依据文中所给出的转换方法构建目标系统的B方法形式化描述,然后利用B方法支持工具对规约进行动态分析和验证,得出可靠的形式规约,为进一步的精化和实现提供正确的起点。最后,文章以当前物流管理中最重要的订单管理系统为例,建立订单管理系统UML类图和状态图,实现系统类图和状态图的B方法形式化描述,并完成系统的模型检测。