Towards a formal semantics for the AADL behavior annex

—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 ing 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- AADL; behavior annex; execution model; TASM

• Type: Conference
• Year: 2009
• Where: DATE
• Authors: Zhibin Yang, Kai Hu, Dianfu Ma, Lei Pi
• Keywords: AADL Execution Model, Behavior Annex, DATE 2009, Execution Model, Hardware