随着集成电路产业的发展,计算机的硬件性能在近二十年内迅速提高。硬件以及计算机应用领域的不断扩展,使得人们对软件技术提出更多更高的要求。如何改进软件的质量,提高开发效率成为软件产业的重要研究工作。自90年代面向对象的概念提出以来,由于其可视化、可重用、贴近需求等优点获得了广泛认可,模型也成为沟通用户需求和最终实现的重要桥梁。UML统一并扩展了众多的建模语言,采用丰富的图形作为建模元素。UML的强可读性适用于软件开发的初级阶段,但由于缺乏精确的语义元素,所以在分析、设计和实现时难以建立完整、无二义性的模型,也缺乏必要的精化和验证工具。形式化方法基于严格的数学和逻辑技术,可以对软件系统进行规约、设计和验证,提高安全性与可靠性。形式化的目的是在系统开发的早期阶段发现并消除不一致、不明确或不完整现象。逻辑精确的语义使开发者与用户形成对需求的一致理解,消除了模糊、不一致；语义的验证自动化,提高了系统的可靠性和效率。然而,由于对设计者提出了数学和逻辑的要求,所以形式化方法在应用领域上存在局限性,很难普及。理想的软件开发是对可视化建模技术和形式化方法的结合。本文研究UML的动态语义,在保证易读性的基础上,增添必要的语义元素,保证模型的无歧义和可验证性,主要研究成果如下：(1)使用抽象状态自动机对UML活动图进行语义规约。首先定义了活动图的静态语义,分别对动作节点(原子节点)、分支节点、并发节点和活动节点分别给出了语义规约,并递归产生了抽象自动机活动图的规约。随后通过规则对活动图的动态行为,如分支、汇合以及触发捕获事件等行为给出了相应的语义规约。在工作流的循环鉴别器模型中,采用这种方法更为清晰地规约了语义。(2)使用抽象状态自动机对UML状态图进行语义规约。作为UML中描述行为的重要图形,状态图涵盖了对象在其生命周期内的全部转换形态。本文首先给出了状态图的静态语义,规约了迁移及状态的语义,然后在UML状态图的基础上,给出了扩展的抽象状态自动机模型,提出了基于扩展模型的状态图行为语义。(3)使用抽象状态自动机对UML顺序图进行语义规约。定义了顺序图中消息和对象的语义规约,随后,针对图形中消息传送条件不明确,时序不清晰的问题,为顺序图的消息传送行为进行了规约。根据前面给出的状态图和顺序图的语义规约,对电梯实例的UML动态模型进行了语义归约和规则验证,消除了在递归调用中可能出现的死锁和不一致。(4)提出了UML动态图的π增量精化体系。先给出了π演算对UML动态图的语义规约,将动态图中的各个元素分别映射到π演算的进程和通道；然后规约了动态图的各种动态要素,如状态的不同转换模式、各种消息的传送行为等的语义规约。最后利用弱互模拟关系,定义了顺序图和状态图的行为等价性判别标准；提出了最大弱互模拟集、替换规则,并藉此给出了在精化模型上进行增量一致性检测的方法,电话系统的实例表明,这种方法大大提高了验证的效率。