文献详情
Exploring AADL verification tool through model transformation
文献类型期刊
作者Hu, Kai[1];Zhang, Teng[2];Yang, Zhibin[3];Tsai, Wei-Tek[4]
机构
通讯作者Zhang, T (reprint author), Beihang Univ, Sch Comp Sci & Engn, Beijing 100191, Peoples R China.
2015
期刊名称JOURNAL OF SYSTEMS ARCHITECTURE影响因子和分区
来源信息年:2015  卷:61  期:3-4  页码范围:141-156  
61
期刊信息JOURNAL OF SYSTEMS ARCHITECTURE影响因子和分区  ISSN:1383-7621
3-4
关键词Real-time system; AADL; TASM; Model transformation; Translation rules
页码范围141-156
增刊正刊
摘要Architecture Analysis and Design Language (AADL) is often used to model safety-critical real-time systems. Model transformation is widely used to extract a formal specification so that AADL models can be verified and analyzed by existing tools. Timed Abstract State Machine (TASM) is a formalism not only able to specify behavior and communication but also timing and resource aspects of the system. To verify functional and nonfunctional properties of AADL models, this paper presents a methodology for translating AADL to TASM. Our main contribution is to formally define the translation rules from an adequate subset of AADL (including thread component, port communication, behavior annex and mode change) into TASM. Based on these rules, a tool called AADL2TASM is implemented using Atlas Transformation Language (ATL). Finally, a case study from an actual data processing unit of a satellite is provided to validate the transformation and illustrate the practicality of the approach. (C) 2015 Elsevier B.V. All rights reserved.
收录情况SCIE(WOS:000353861800001)  EI(20151400699739)  
所属部门计算机学院
DOI10.1016/j.sysarc.2015.02.003
百度学术Exploring AADL verification tool through model transformation
语言外文
ISSN1383-7621
被引频次44
人气指数34
浏览次数34
基金National Natural Science Foundations of China [61073013]; State Key Laboratory of Software Development Environment [SKLSDE-2014ZX-09]; Aviation Science Foundation of China [2012ZC51025]
全部评论(0 条评论)
作者其他论文

An evaluation framework for software crowdsourcing.

Wu, Wenjun;Tsai, Wei-Tek;Li, Wei.FRONTIERS OF COMPUTER SCIENCE.2013,7(5),694-709.

基于时间抽象状态机的AADL模型验证?.

杨志斌;胡凯;赵永望,等.软件学报.2015,202-222.

Test algebra for combinatorial testing.

Tsai, Wei-Tek;Colbourn, Charles J.;Luo, Jie,等.2013 8th International Workshop on Automation of Software Test, AST 2013.2013,19-25.

The Design and Implementation of an Extended 1553B Bus IP Core to Support Large File Transfer.

Hu, Kai;Liu, Kai;Liu, Cheng.2012 7TH INTERNATIONAL CONFERENCE ON COMPUTING AND CONVERGENCE TECHNOLOGY (ICCCT2012).2012,494-498.

Simulation of real-time systems with clock calculus.

Hu, Kai;Zhang, Teng;Yang, Zhibin,等.SIMULATION MODELLING PRACTICE AND THEORY.2015,51,69-86.

登录