OATAO - Open Archive Toulouse Archive Ouverte Open Access Week

Exploring AADL verification tool through model transformation

Hu, Kai and Zhang, Teng and Yang, Zhibin and Tsai, Wei-Tek Exploring AADL verification tool through model transformation. (2015) Journal of Systems Architecture, vol. 61 (n° 3-4). pp. 141-156. ISSN 1383-7621

[img]
Preview
(Document in English)

PDF (Author's version) - Requires a PDF viewer such as GSview, Xpdf or Adobe Acrobat Reader
1MB

Official URL: http://dx.doi.org/10.1016/j.sysarc.2015.02.003

Abstract

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.

Item Type:Article
Additional Information:Thanks to Elsevier editor. The definitive version is available at http://www.sciencedirect.com The original PDF of the article can be found at Journal of Systems Architecture website : http://www.sciencedirect.com/science/article/pii/S1383762115000144
HAL Id:hal-01285662
Audience (journal):International peer-reviewed journal
Uncontrolled Keywords:
Institution:French research institutions > Centre National de la Recherche Scientifique - CNRS (FRANCE)
Université de Toulouse > Institut National Polytechnique de Toulouse - INPT (FRANCE)
Université de Toulouse > Université Paul Sabatier-Toulouse III - UPS (FRANCE)
Université de Toulouse > Université Toulouse - Jean Jaurès - UT2J (FRANCE)
Université de Toulouse > Université de Toulouse I-Sciences Sociales - UT1 (FRANCE)
Other partners > Arizona State University - ASU (USA)
Other partners > Beihang University (CHINA)
Other partners > Nanjing University of Aeronautics and Astronautics – NUAA (CHINA)
Laboratory name:
Statistics:download
Deposited By: IRIT IRIT
Deposited On:09 Mar 2016 14:35

Repository Staff Only: item control page