Exploring AADL verification tool through model transformation

Kai Hu, Teng Zhang, Zhibin Yang, Wei Tek Tsai

Research output: Contribution to journalArticle

12 Citations (Scopus)

Abstract

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.

Original languageEnglish (US)
Article number1267
Pages (from-to)141-156
Number of pages16
JournalJournal of Systems Architecture
Volume61
Issue number3-4
DOIs
StatePublished - 2015

Fingerprint

Communication
Real time systems
Satellites
Formal specification

Keywords

  • AADL
  • Model transformation
  • Real-time system
  • TASM
  • Translation rules

ASJC Scopus subject areas

  • Hardware and Architecture
  • Software

Cite this

Exploring AADL verification tool through model transformation. / Hu, Kai; Zhang, Teng; Yang, Zhibin; Tsai, Wei Tek.

In: Journal of Systems Architecture, Vol. 61, No. 3-4, 1267, 2015, p. 141-156.

Research output: Contribution to journalArticle

Hu, Kai ; Zhang, Teng ; Yang, Zhibin ; Tsai, Wei Tek. / Exploring AADL verification tool through model transformation. In: Journal of Systems Architecture. 2015 ; Vol. 61, No. 3-4. pp. 141-156.
@article{4b89eba60b7c478295403c8aa1caacef,
title = "Exploring AADL verification tool through model transformation",
abstract = "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.",
keywords = "AADL, Model transformation, Real-time system, TASM, Translation rules",
author = "Kai Hu and Teng Zhang and Zhibin Yang and Tsai, {Wei Tek}",
year = "2015",
doi = "10.1016/j.sysarc.2015.02.003",
language = "English (US)",
volume = "61",
pages = "141--156",
journal = "Journal of Systems Architecture",
issn = "1383-7621",
publisher = "Elsevier",
number = "3-4",

}

TY - JOUR

T1 - Exploring AADL verification tool through model transformation

AU - Hu, Kai

AU - Zhang, Teng

AU - Yang, Zhibin

AU - Tsai, Wei Tek

PY - 2015

Y1 - 2015

N2 - 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.

AB - 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.

KW - AADL

KW - Model transformation

KW - Real-time system

KW - TASM

KW - Translation rules

UR - http://www.scopus.com/inward/record.url?scp=84925869140&partnerID=8YFLogxK

UR - http://www.scopus.com/inward/citedby.url?scp=84925869140&partnerID=8YFLogxK

U2 - 10.1016/j.sysarc.2015.02.003

DO - 10.1016/j.sysarc.2015.02.003

M3 - Article

AN - SCOPUS:84925869140

VL - 61

SP - 141

EP - 156

JO - Journal of Systems Architecture

JF - Journal of Systems Architecture

SN - 1383-7621

IS - 3-4

M1 - 1267

ER -