随着计算机应用领域的不断扩张,计算机软件的开发规模逐渐扩大,软件复杂度不断增加,开发周期和开发成本也不断增长。为了解决这些问题,对象管理组织(OMG)提出了模型驱动结构方法(Model Driven Architecture)。MDA的核心思想是以模型为中心,将模型和实现分离,使软件开发过程简化为建立业务逻辑模型后由机器自动生成特定计算平台的代码。在MDA中,建模语言不仅仅是设计语言,也是编程语言。针对嵌入式领域中的软件开发复杂度问题,业界提出一种基于MDA方法的体系结构建模语言-体系结构分析设计语言(Architecture Analysis and Design Language, AADL).AADL是用于设计和分析安全关键的嵌入式实时系统的软件和硬件体系结构的建模语言,围绕AADL的开发平台及模型验证工具的开发逐渐成为热点。MDA的核心是模型,而模型设计是否满足需求则需要其它工具来进行测试验证。本论文基于带时钟约束的混合自动机理论,设计了一种对AADL模型的可调度性进行形式化验证的工具。论文首先介绍了目前关于AADL模型的可调度性验证的研究情况及已开发的工具,并分析了各种工具的缺陷。然后简要介绍了AADL的概念及时间自动机理论。在此基础上,对使用UPPAAL工具对AADL模型进行可调度性验证进行了实践。实践表明UPPAAL工具无法进行可抢占调度策略下的AADL模型的可调度性验证。因此,论文在带时钟约束的混合自动机理论基础上进行了AADL可调度性验证工具UCaS的设计开发。论文按照软件工程方法分模块详细说明UCaS的设计、涉及的技术及关键代码,并对UCaS工具的性能进行了测试。论文最后总结了UCaS工具的优点及局限性,对AADL模型验证工具的后继研究和发展进行了展望。