Abstract: AADL (architecture analysis and design language) is a modeling language to describe complex embedded systems and is widely used to model and verify safety-critical systems. AADL enables modeling of component inner behavior in a state-machine based on behavior annex. Hierarchical automata are always used in complex systems in industry to describe the functional behavior of components, but there is no mechanism to represent hierarchical automata in behavior annex. Aiming at this problem, this paper proposes a hierarchical extension of AADL behavior annex which is named HBA (hierarchical behavior annex). To begin with, this paper gives the syntax of HBA, and then it defines the semantics of HBA. This paper proposes a meta-model of HBA and implements its textual and graphical editor in the OSATE environment. In order to facilitate formal verification, the transformation rules from HBA to timed automata (TA) are given, and formal verification is carried out based on the model checker UPPAAL. Finally, a case study is presented to verify the effectiveness of the proposed method.

Key words: safety-critical system, architecture analysis and design language (AADL), hierarchical behavior annex(HBA), functional specification

摘要： 架构分析与设计语言（AADL）是一种用于描述复杂嵌入式系统体系架构的建模语言，被广泛用于安全关键系统建模与验证。AADL通过行为附件以状态机的形式对组件的内部行为建模。工业界中的复杂系统常使用层次自动机描述组件的功能行为，而行为附件中没有表达层次自动机的机制。针对这一问题，提出了AADL行为附件的层次化扩展——HBA。首先给出了HBA的形式语法，然后定义了HBA的操作语义。提出了HBA的元模型，并在OSATE环境中实现其文本和图形化编辑器。为了便于形式化验证，给出了HBA到时间自动机（TA）的转换规则，并基于模型检测工具UPPAAL进行形式化验证。最后，给出一个案例研究来验证所提方法的有效性。

关键词: 安全关键系统, 架构分析与设计语言（AADL）, 层次行为附件（HBA）, 功能规约