实时系统已广泛应用于国防、航空航天、通信、自动控制等领域。随着实时系统的规模和复杂性的增加,为了更好地理解所开发的系统,从而开发出高质量的实时软件,需要对系统进行建模。UML已经成为大规模复杂软件系统建模的工业标准,在实时软件开发中也得到了广泛的应用。使用UML对软件建模时经常会出现模型之间的不一致性问题,需要在软件开发的早期阶段检测并消除模型之间的不一致性。在上述研究背景之下,本文研究了在实时软件开发的早期阶段,对使用UML2.0顺序图和状态图建立的实时软件动态行为模型之间的一致性进行验证的问题,所验证的一致性包括语法一致性和语义一致性。实时系统计算的正确性不仅取决于程序的逻辑正确性,也取决于结果的产生时间,如果系统的时间约束条件得不到满足,将会发生系统出错,因此在语义一致性验证中本文研究了行为一致性验证和时间一致性验证。具体研究内容如下:(1)给出了UML顺序图和状态图在语法和语义上的形式化描述,后面的分析和验证就是基于该形式化描述。(2)分析了顺序图中事件之间的关系,提出了一种使用自动机来描述每个对象在顺序图描述的场景中所参与的事件的方法,并将该方法扩展到带有组合片段的UML2.0顺序图,分析了UML2.0顺序图中的时间建模机制,研究了从UML2.0顺序图中提取时间约束的算法。(3)对UML2.0状态图扩充时间性质以便于对实时软件建模,在此基础上,给出了一种使用UML2.0状态图网络建模实时软件动态行为的方法,研究了从状态图网络到时间自动机网络的转化方法,从而便于使用模型检测工具UPPAAL对其进行进一步的分析与验证。(4)基于以上研究,提出了实时软件顺序图模型和状态图模型的语法一致性、行为一致性和时间一致性的验证方法,最后,结合汽车档位控制器系统实例,说明了本文所提出的一致性验证方法。