随着技术的发展和人们需求的不断提高,实时系统的复杂度在不断地增长,为实时系统的开发带来了巨大挑战。本文在异步扩展层次自动机(Asynchronous Extended Hierarchical Automata, ASEHA)上,引入了时钟变量,在迁移和位置上增加了时钟约束,给出了一种具有时间扩展的ASEHA模型,有效降低了实时系统建模的复杂性,利用模型检测工具UPPAAL,对 ATM(Automatic Teller Machine)系统和旅游预订票Web服务系统进行检验,验证了系统无死锁、可达性、活性、安全性等性质。本文所取得的主要成果有:　　(1)针对实时系统,给出了一种基于时间扩展的ASEHA模型。将实时系统建模为具有时间扩展的ASEHA模型,以ATM系统为例阐述了建模过程,利用UPPAAL工具检验该系统的可达性等性质,最后验证表明该模型是正确的、安全的。　　(2)针对带时间约束的组合W eb服务系统,给出了一种模型检测方法。将组合W eb服务的描述语言BPEL4WS转化成基于时间扩展的ASEHA语言,对组合Web服务建立形式化模型,采用模型检测工具UPPAAL对系统的实时性和可信性进行验证,从而保证了系统模型的实效性与安全性。　　(3)基于本文提出的具有时间扩展的ASEHA对带时间约束的组合Web服务系统验证的方法,分析了旅游预订票W eb服务系统,给出了该系统的BPEL4WS描述语言转化为时间扩展的ASEHA语言代码和形式化定义描述,建立了基于时间扩展的ASEHA模型,利用模型验证工具UPPAAL对该系统进行检验与分析,验证了其无死锁、安全性及活性等性质。