随着信息技术的高速发展,实时系统的应用范围变得越来越广泛。要正确的设计出一个实时系统,就要在分析实时系统的早期给出实时系统的正确模型。统一建模语言UML正是用来对复杂系统进行建模的。UML模型分为静态结构模型和动态行为模型两类,静态模型关注系统的结构信息,而动态结构模型关注系统的行为信息。一般而言,UML动态行为模型往往更加复杂和重要。使用UML为实时系统的动态行为建模的方法是本文的研究内容之一。同时,实时系统的实时行为可以用时间约束条件来描述,但UML是一种图形化的语言,它的语义使用自然语言描述的,存在不精确性。因此,形式化的语义就成了UML的一个迫切需求。把UML和形式化语言进行融合,通过形式化的方法来弥补UML语义上的不足,给出实时行为方面模型的精确语义,也是本文的研究重点。本文工作主要内容归纳如下:首先,对UML2新增图之一交互概观图进行了研究,提出了一种基于交互概观图对实时式系统进行建模的方法,并通过一个具体建模实例来说明这种方法。此方法与通常的建立动态行为模型方法相比更加直观和全面,能从整体上把握系统的动态行为。然后,在前人研究的基础上给出了UML顺序图和时间约束属性相关方面的形式化定义,包括简单顺序图、带组合片段的顺序图和时间约束同一性。并对顺序图扩充时间性质以便于描述实时系统。精确的形式化描述是整个研究的基石,后面的分析和验证都基于该形式化描述。最后,对带组合片段的顺序图满足时间约束同一性的定理进行了证明,并以此定理为基础对带时间约束属性的UML顺序图提出了一种验证算法,判断其是否符合某些时间约束属性。带时间约束属性的顺序图为实时系统的建模提供了便利,通过检验系统的行为是否满足某种时间约束属性,能够提高实时系统的安全性。