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

Functional Behavior Modeling Extension of System Architecture Description Language AADL

作　　者：许金淼 杨志斌[1,2] 黄志球 谢健[1,2] 周勇 XU Jinmiao;YANG Zhibin;HUANG Zhiqiu;XIE Jian;ZHOU Yong(School of Computer Science and Technology,Nanjing University of Aeronautics and Astronautics,Nanjing 210016,China;Key Laboratory of Safety-Critical Software,Ministry of Industry and Information Technology,Nanjing 210016,China)

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

出　　处：《计算机科学与探索》2019年第10期1638-1653,共16页Journal of Frontiers of Computer Science and Technology

基　　金：国家自然科学基金;国家重点研发计划;GF基础科研重点项目;江苏省自然科学基金;中央高校基本科研业务费专项资金~~

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

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

分 类 号：TP311[自动化与计算机技术—计算机软件与理论]