摘要
架构分析与设计语言(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.
作者
许金淼
杨志斌
黄志球
谢健
周勇
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)
出处
《计算机科学与探索》
CSCD
北大核心
2019年第10期1638-1653,共16页
Journal of Frontiers of Computer Science and Technology
基金
国家自然科学基金
国家重点研发计划
GF基础科研重点项目
江苏省自然科学基金
中央高校基本科研业务费专项资金~~