随着硬件设备计算能力的迅速提高以及社会需求的不断变化和增长,嵌入式系统变得越来越复杂,这对嵌入式实时软件开发的各个阶段(从系统分析、设计到实现、验证)均带来了新的困难和挑战。为了保障嵌入式实时软件的实时性、安全性和可靠性等,本文将基于UML的建模方法与形式化建模方法相结合,为嵌入式实时软件的建模和验证提供一种解决方案。UML2.0顺序图是UML的中描述能力最强的视图之一,它着重体现对象间动态的交互关系,并且还具有良好的易理解性。但是UML2.0顺序图用来对嵌入式实时软件建模和验证还存在时间描述方面不足之处。因此提出一种利用UML的扩展机制对UML2.0顺序图进行扩展的方法。扩展后的UML2.0顺序图不但能够很好的保持原来的易理解性,而且能够清晰的描述嵌入式实时软件的时间需求。根据扩展后UML2.0顺序图与时间自动机的语义,提出一种将扩展后UML 2.0顺序图转换成时间自动机的方法,从而将UML 2.0顺序图与时间自动机结合起来,利用UML2.0顺序图对嵌入式实时软件建模,转换成时间自动机后利用工具加以验证。最后通过对一个电梯管理系统建模和验证,把本文提出的结合思想运用到实例系统的验证当中。本文的研究对嵌入式实时软件建模和验证、UML2.0顺序图的应用和形式化方法在软件验证过程中的使用都有一定的推动作用。