:结构分析和设计语言(architectureanalysis anddesignlanguage)是嵌入式实时系统的一种体系结构描述语言标准,广泛应用于航空宇航工业中对安全关键应用系统模型的建模。本文首先归纳了AADL的发展历程及其主要建模元素。其次,介绍了模型检测方法的研究和应用,并就航电系统与模型检测方法做了研究和分析。最后,探讨了AADL 模型转化为形式化模型,并用模型检测方法进行验证和分析的方法和可行性。嵌入式实时系统AADL建模形式化方法模型验证