期刊名称：Journal of Software Engineering and Applications
印刷版ISSN：1945-3116
电子版ISSN：1945-3124
出版年度：2013
卷号：6
期号：3
页码：147-155
DOI：10.4236/jsea.2013.63019
出版社：Scientific Research Publishing
摘要：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.
