Toolchain Based on MDE for the Transformation of AADL Models to Timed Automata Models

• 作者: Allaoui Chaoui Martin Strecker Mohamed El-Kamel Hamdane
• 来源期刊: 软件工程与应用(英文)
• 学科: 数学
• 关键词: AADL TIMED AUTOMATA Transformation Verification UPPAAL
• 年，卷（期）: rjgcyyyyw_2013,（3）
• 页码范围: 147-155
• 页数: 9页
• 分类号: O1

摘要

In this work, we propose an approach for the verification of the AADL architecture. This approach is based on Model Driven Engineering (MDE) and assisted by a toolchain. Indeed, we define a source meta-model for AADL and a target meta-model for the timed automata formalism;we define a transformation process in two steps: the first is a Model2 Model transformation which takes an AADL Model and produces the corresponding timed automata model. The second transformation is a Model2 Text transformation which takes a timed automata model and generates a text in ta-format code. This code is accepted by the Uppaal toolbox. A case study has been developed to show the feasibility and validity of the proposed approach.