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

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