Towards a formal semantics for the AADL behavior annex

Author

Yang, Zhibin ; Hu, Kai ; Ma, Dianfu ; Pi, Lei

Author_Institution

Sch. of Comput. Sci. & Eng., Beihang Univ., Beijing

fYear

2009

fDate

20-24 April 2009

Firstpage

1166

Lastpage

1171

Abstract

AADL is an Architecture Description Language which describes embedded real-time systems. Behavior annex is an extension of the dispatch mechanism of AADL execution model. This paper proposes a formal semantics for the AADL behavior annex using Timed Abstract State Machine (TASM). Firstly, the semantics of AADL default execution model is given, and then we formally define some aspects semantics of behavior annex. A prototype of real-time behavior modeling and verification is proposed, and finally, a case study will be given to validate the feasibility.

Keywords

finite state machines; formal verification; high level languages; program compilers; programming language semantics; software architecture; specification languages; AADL behavior annex; AADL default execution; AADL execution model; TASM; architecture description language; automotive engineering; dispatch mechanism; embedded real-time system; formal semantics; real-time behavior modeling; timed abstract state machine; verification; Architecture description languages; Automotive engineering; Computer science; Design engineering; File servers; Prototypes; Real time systems; Runtime environment; Timing; AADL; TASM; behavior annex; execution model;

fLanguage

English

Publisher

ieee

Conference_Titel

Design, Automation & Test in Europe Conference & Exhibition, 2009. DATE '09.

Conference_Location

Nice

ISSN

1530-1591

Print_ISBN

978-1-4244-3781-8

Type

conf

DOI

10.1109/DATE.2009.5090839

Filename

5090839