通用建模语言(UML, Unified Modeling Language),是一种功能强大的、可视化面向对象建模语言,它提供了多种UML子图,可以刻画系统的不同侧面,包括静态拓扑结构、动态行为、组装方式等。经过几十年的发展,在系统建模领域,设计开发人员普遍采用UML建立系统模型,现在UML已经成为事实的工业标准。UML存在于软件生命周期的各个阶段：需求、设计、分析、实现、测试、发布、维护等。对一些安全关键系统,如网络协议、轨道交通控制系统、嵌入式实时并发系统等,在需求、设计阶段前期,要求保证系统模型的关键功能性属性,和推导量化的非功能属性。设计开发人员通常采用UML建模复杂系统,但是,UML是一种半形式化的元模型,不具备精确的形式语义,不能对关键系统属性进行自动推理。如果能给UML赋予形式化语义,就能在模型检测器的支持下,对关键系统属性,自动进行功能验证和性能分析。静态UML子图用于刻画系统的拓扑结构,动态UML子图用于刻画系统行为,设计开发人员,通常更关注系统运行时(run-time)特性。本文的研究工作,主要是给动态UML子图赋予形式语义,关注的问题有：UML的语义描述不精确,造成需求和设计之间、设计和实现之间,存在着歧义；在描述一个系统时,不同类型的UML子图之间,可能存在语义不一致,甚至位于不同抽象层次的、同一类型的UML图元之间,也可能存在语义冲突；对某些概率、比率、时间相关的实时并发系统,UML的建模和验证能力不足。进程代数(Process Algebras),用代数理论研究通信并发系统。进程代数基于标签迁移系统,用一组算子作为基本成分,用算子间的组合刻画复杂系统。进程代数的核心是：互模拟等价理论,即在何种意义下,两个进程的行为相同。首先,标签迁移系统能够描述UML状态图／序列图的动态行为,其次,互模拟等价理论,为检测不同UML图元之间的语义等价性,提供了理论基础。概率模型检测(Probabilistic Model Checking),支持离散时间Markov链和连续时间Markov链,适于建模概率、比率、时间相关的实时并发系统。概率模型检测由英国伯明翰大学首先提出,并提供模型检测器PRISM支持,适合于建模和验证概率、比率相关的实时模型,对系统关键量化性能指标,实现自动推导和分析。本文在动态UML子图形式化方面,进行了研究,主要研究内容和创新点概括如下：1.给UML状态图／序列图赋予LTS操作语义UML状态图／序列图,由基本构成元素和若干种组装方式(或组合片段)构成。UML状态图/序列图被抽象为一个数学模型,LTS结构被提取为另外一个数学模型。对UML状态图/序列图的基本构成元素,本文给出了其到LTS结构的映射规则；对UML状态图/序列图的组装方式(或组合片段),本文给出了其LTS操作语义,及转换规则。首先给UML状态图/序列图赋予LTS操作语义,而非直接转换为某种进程代数规范,这样做的好处是：因为进程代数是基于LTS结构,所以,如果给定LTS操作语义,就可以根据不同的语法,将其转换为任意一种进程代数形式规范,而非某一种进程代数形式规范。把UML状态图/序列图转换为某一种进程代数形式规范后,如pi演算,基于互模拟等价理论,在工具的支持下,可以验证不同UML图元之间的语义一致性、系统死锁性；通过工具的单步执行,可以观察系统的动态运行情况,以验证需求和设计是否一致。针对基于pi演算的UML序列图,本文分析并推导了：验证互模拟等价性、系统死锁性算法的时间复杂度,给出了定理、证明和结论。2.给扩展的UML状态图赋予概率/随机Kripke结构语义UML状态图在经过扩展之后,和概率模型检测的语法和语义,具有隐式的映射关系,适合于建模概率、比率相关的实时并发系统。扩展的UML状态图被抽象为一个数学模型,概率/随机Kripke结构被定义为另外一个数学模型,给出了映射规则和转换算法,实现了这两种数学模型之间的转换。扩展的UML状态图,由基本构成元素和若干组装方式构成,这样做的好处是：便于使用数学归纳法,对转换算法的正确性进行分析。给UML状态图赋予概率/随机Kripke结构语义后,可以建模和验证实时并发系统,如排队网络、Ad Hoc概率网络等。在模型检测工具PRISM支持下,可以对量化性能指标,进行自动分析和推导；也可通过PRISM单步执行,观测概率、实时系统的动态运行情况。3.提取关键XMI标签及其数据结构,给出形式语义生成算法通常,在给UML赋予形式语义的研究工作,都是在较高抽象层次上,给出从UML图元到形式语义的转换规则和算法。但是,在设计和实现UML形式语义转换器时,需要对动态UML子图导出的XMI文件进行解析,所以,形式语义生成算法,和存储了关键数据/结构信息的XMI标签紧密相关。本文不但在较高层次上,给出了UML子图的操作语义和转换规则,而且提取出关键XMI标签,将其抽象为数据结构,较低抽象层次上,给出了XMI标签相关的形式语义生成算法,可用于设计实现UML形式语义转换器。4.设计并实现了UML形式语义转换器原型工具在Eclipse集成开发环境下,使用Java语言和Xerces解析器,设计并实现了一个UML形式语义转换器原型工具,给UML状态图／序列图赋予LTS形式语义,或概率／随机Kripke形式语义,最后转换为pi演算代码或PRISM代码。软件原型工具采用了多层体系架构：XMI文件解析→关键数据/结构信息存储→形式语义生成→形式规范转换,增强了软件工具的健壮性、可移植性和可扩展性。