随着嵌入式系统的规模、复杂程度和可靠性需求的不断提升，模型驱动的体系结构开发方法已经成为复杂嵌入式系统开发的主流。体系结构分析与设计语言AADL（ArchitectureAnalysisand Design Language, AADL）是嵌入式实时系统领域模型驱动方法的新标准，在支持系统软、硬件结构建模的同时可对可靠性、实时性等非功能属性的描述，可在模型驱动开发过程早期的模型建立阶段，通过形式化的模型检验方法对系统模型的关键属性进行验证，及早发现设计过程中潜在的错误，对保障系统实时性和提高开发效率都具有重要的意义。为了对AADL模型的可调度性和数据流时延特性进行验证，本文采用时间自动机形式化模型检验方法建立了AADL模型中调度模型和数据流的时间自动机，实现了从AADL模型到时间自动机模型的转换和验证工作。在调度模型时间自动机的建立中，设计了周期、非周期的线程模板以及抢占和非可抢占的调度器模板，通过模型转换法则将AADL调度模型转换到时间自动机模型。在数据流的模型转换中，分别设计了单一数据流和混合数据流到时间自动机的转换方法，混合数据流转换得到的时间自动机可与调度模型时间自动机构成时间自动机网络，实现了数据流与调度模型的综合分析与验证。利用Eclipse的插件开发技术，设计了自动化模型转换插件并将其集成到AADL的建模工具OSATE中，实现了建模、转换、验证与分析过程的集成开发环境。最后利用时间自动机建模与验证工具UPPAAL对转换得到的时间自动机进行模拟和验证，等价地验证原AADL模型的设计是否满足实时性要求。测试数据表明，所建立模型转换方法能有效地将AADL模型转换到时间自动机模型，在UPPAAL中能够正确地分析原模型的可调度性和数据流时延特性。