Journal of Frontiers of Computer Science and Technology ›› 2019, Vol. 13 ›› Issue (10): 1638-1653.DOI: 10.3778/j.issn.1673-9418.1808053

Previous Articles     Next Articles

Functional Behavior Modeling Extension of System Architecture Description Lan-guage AADL

XU Jinmiao, YANG Zhibin, HUANG Zhiqiu, XIE Jian, ZHOU Yong   

  1. 1.School of Computer Science and Technology, Nanjing University of Aeronautics and Astronautics, Nanjing 210016, China
    2.Key Laboratory of Safety-Critical Software, Ministry of Industry and Information Technology, Nanjing 210016, China
  • Online:2019-10-01 Published:2019-10-15

系统架构描述语言AADL的功能行为建模扩展

许金淼杨志斌黄志球,谢  健,周勇   

  1. 1.南京航空航天大学 计算机科学与技术学院,南京 210016
    2.高安全系统的软件开发与验证技术工信部重点实验室,南京 210016

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), 功能规约