目前软件工业界面临着产品功能越来越复杂和推出产品周期越来越短的双重压力。软件工程的一个主要目标就是在软件复杂性增加的情况下仍能构造正确可靠的系统,达到这一目标的途径之一就是形式化方法。形式化方法是一种用于规范、设计和验证计算机系统的基于数学的方法,包括各种语言、技术和工具等。使用形式化方法采用逐步渐进的方式来开发,可以提高软件可靠性和生产效率,实现软件自动化。统一建模语言UML已成为面向对象软件系统中描述分析和设计阶段模型的标准化记法,但UML在某些方面仍存在不足,首先,UML只是一种建模语言,而不是一种方法,因此在实际的开发和设计中,需要具体的过程技术来支持。其次,复杂系统的建模往往需要进行严格的语义分析,而UML缺乏精确的语义,因此对模型难以进行一致性检查和正确性分析,成为基于UML技术的严重缺陷。针对以上问题,本文提出了基于统一过程的UML到形式化的系统转换思想,将统一过程RUP、UML、形式化方法三者结合用于软件系统建模中。其中UML作为支持建模语言,其图形表示直观易理解;RUP作为建模中的方法指导,它与UML在实际开发过程中的结合,使系统的分析和设计过程变得清晰,降低了系统的开发风险;对UML进行形式化转换研究,可以将UML与形式化语言的的准确性、一致性结合起来,为模型的正确性证明、转换及一致性检查提供有力的理论方法。本文选择形式化方法中一种比较成熟的方法---B方法来描述UML模型图,B方法与其他形式化方法相比具有很多优点:B方法支持从软件需求规格说明、设计到最后实现的整个软件开发过程,并具有B-Toolkit、Atelier B、ProB等工具的全面支持。本文主要针对UML模型图中的用例图、类图、顺序图提出其到形式化B方法的转换机制,并对已存在的状态图的转换机制进行扩充,使其针对于某些特定的事例。对一个复杂的软件系统,软件开发人员可以在统一过程的指导下,通过UML中的各种图对目标系统进行建模,然后根据文中UML-B的转换方法,构建目标系统的B机器,从而建立一种从图形加文字的半形式化模型到具有数学基础的形式化模型的系统映射,在此基础之上,可以进一步地进行模型检测、正确性验证、代码半自动生成等工作。最后,结合了一个免疫系统中细胞免疫的实例,使用并验证了UML模型到B的系统转换方法,并在B方法支持工具(ProB)中对所得到的形式化模型进行了动态分析和模型检测,以保证规格说明的正确性和可靠性。