Unified Modeling Language(UML,统一建模语言)是一种基于面向对象建模方法组合的建模语言。它以支持面向对象、可视化建模和强大的表达能力等优点已经成为人们构建大型超大型系统模型的首选语言。大多数UML规范都是描述性的,易于理解,但它们不是形式化的描述语言,它们的语法结构使用形式化规约,却缺乏精确的语义,经常产生模糊或者歧义,无法保证软件的正确性和可靠性。因此,为了增强该语言的准确性、一致性和可扩展性,保证系统的正确性并且降低软件开发的成本和后期的运行和维护风险,我们特别需要对UML进行形式化研究。本文首先讨论了一种从UML到Object-Z的映射方法。Object-Z作为一种形式化语言,引入了类的概念,能够较好地为UML元模型层上的各类图形中的语法和静态语义进行形式化描述。本文使用Object-Z语言对UML类图的语法和语义进行了形式化映射,并且用实例验证了该映射的可行性和正确性。然后,本文试图寻找一种从Object-Z到可执行代码的映射,将Object-Z形成的“伪代码”变成可被计算机识别和运行的可执行代码。本文发现Python作为现在越来越热门的编程语言,由于其独特的语法特点、优良的代码可移植性,最关键是和Object-Z语言有很多相似性,使得它自然而然成为我们转换Object-Z伪代码的一种极好的语言。在转换过程中,我们使用契约式设计,保证了Object-Z规约和Python代码之间的一致性,从而确保了该映射过程的正确性。通过该工作,我们找到了一种将UML类图形式化为Object-Z规约,最后从Object-Z规约映射为Python可执行代码的方式,这将为提高软件开发特别是复杂大型系统的开发效率提供了一种可行的方法。