计算机技术与发展2017，Vol.27Issue(3)：23-28,6.DOI:10.3969/j.issn.1673-629X.2017.03.005
基于Z-AADL模型的形式化转换
Formal Transformation Basedon Z-AADL Model
摘要
Abstract
Architecture Analysis and Design Language ( AADL) is a kind of system structure modeling language based on model driven development in view of the problem of software development complexity in the field of embedded real-time system,which can be used to design and analyze the software and hardware architecture of some security critical embedded systems. But AADL is a semi-formal mod-eling language seriously. Although it also describes the properties of the components,the non-functional properties of the model are not clearly defined. Therefore,the formal verification of the non-functional properties of the AADL system model is of great significance to guarantee the correctness and reliability of the system. Aiming at the shortage of non-functional and data property of AADL model,com-bining the AADL specification with the Z language,a new specification—Z-AADL is put forward. Then the transformation rules between Z-AADL and ZIA is given,which define that how the Z-AADL model can be transformed to the ZIA model. An example is given to il-lustrate the transformation.关键词
Z-AADL/ZIA/CT-ZIA/模型转换Key words
Z-AADL/ZIA/CT-ZIA/model transformation分类
信息技术与安全科学引用本文复制引用
高正,曹子宁..基于Z-AADL模型的形式化转换[J].计算机技术与发展,2017,27(3):23-28,6.基金项目
国家"973"重点基础研究发展计划项目(2014CB744900) （2014CB744900）
