文献详情
Exploring AADL verification tool through model transformation
文献类型期刊
作者Hu, Kai[1];Zhang, Teng[2];Yang, Zhibin[3];Tsai, Wei-Tek[4]
机构
2015
期刊名称JOURNAL OF SYSTEMS ARCHITECTURE影响因子和分区
通讯作者Zhang, T (reprint author), Beihang Univ, Sch Comp Sci & Engn, Beijing 100191, Peoples R China.
61
来源信息年:2015  卷:61  期:3-4  页码范围:141-156  
3-4
期刊信息JOURNAL OF SYSTEMS ARCHITECTURE影响因子和分区  ISSN:1383-7621
页码范围141-156
关键词Real-time system; AADL; TASM; Model transformation; Translation rules
增刊正刊
摘要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
被引频次2
人气指数31
浏览次数31
基金National Natural Science Foundations of China [61073013]; State Key Laboratory of Software Development Environment [SKLSDE-2014ZX-09]; Aviation Science Foundation of China [2012ZC51025]
全部评论(0 条评论)
作者其他论文

Simulation of real-time systems with clock calculus.

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

Research on SCPS-NP routing protocol.

Jiang, Hong;Hu, Kai.2nd International Conference on Information Engineering and Computer Science, ICIECS 2010.2010.

An analytical model of k-ary n-cube under spatial communication locality.

Hu, Kai;Wang, Zhe.24th IEEE International Conference on Advanced Information Networking and Applications Workshops, WAINA 2010.2010,24-29.

Research on QoS for DVB-RCS satellite networks.

Yang, He;Hu, Kai;Gu, Bin.2nd International Conference on Networking and Distributed Computing, ICNDC 2011.2011,10-14.

Modeling and Verification of Custom TCP Using SDL.

Hu, Kai;Liu, Cheng;Liu, Kai.PROCEEDINGS OF 2013 IEEE 4TH INTERNATIONAL CONFERENCE ON SOFTWARE ENGINEERING AND SERVICE SCIENCE (ICSESS).2012,455-458.

登录