AADL(Architecture Analysis and Design Language)是一种用于描述复杂嵌入式系统体系架构的建模语言国际标准,被广泛用于安全关键系统的建模与验证。AADL通过系统、子系统、进程、线程等组件层次化地表达系统模型。行为附件(Behavior Annex)是AADL在功能行为方面的补充,它通过扁平状态机的形式对组件的内部功能行为以及组件和组件间的交互行为建模。工业界中的复杂系统常使用层次状态机描述组件的功能行为。但是,行为附件中没有表达层次状态机的机制,虽然可以利用AADL自身的分层描述能力对系统建模,但会导致线程的规模过于庞大。在实际的开发过程中,设计者们往往需要将层次化描述的功能需求进行手动扁平化处理,然后借助AADL行为附件对其建模,这个过程是繁琐的且易错的,并且扁平化的状态机会造成结构信息的丢失,无法直观的表示功能行为模块的包含层次关系。针对AADL行为附件不能以层次化的形式建模功能行为这一问题,本文提出了一种基于AADL行为附件的功能行为层次化建模及验证方法,包括基于扩展的AADL层次行为附件建模方法和层次行为附件的形式化验证方法两部分。为了适应工业界的实际建模需求,本文首先提出了AADL行为附件的层次化扩展——层次行为附件HBA,给出了HBA的形式语法,定义了HBA的操作语义,提出了HBA的元模型,并在OSATE环境中实现其文本和图形化编辑器。为了对所建模型进行形式化验证,本文提出了层次行为附件的形式化验证方法。首先通过层次行为附件扁平化方法将层次行为模型转化为多个相关联的扁平状态机,然后通过层次行为附件到时间自动机的转换方法将层次行为模型转换为时间自动机网络,最后人工抽取与被验模型相关属性,并将待验证模型与待验证属性输入到UPPAAL中,对所建模型进行验证。最后,通过一个航天器导航、制导与控制系统案例来验证本文所提方法的有效性。首先通过详细描述建模过程、逐步精化原始需求的方式,检验本文所提建模方法是否适用于建模实际工业案例;然后通过在原始需求中预埋错误的方式,检验本文所提出的HBA形式化验证方法是否可以检测出所建模型与待验证属性存在不一致的问题。