Research ArticleOpen AccessGoogle Scholar indexed
Toolchain Based on MDE for the Transformation of AADL Models to Timed Automata Models
Department of Computer Science, Normal High School of Constantine, Constantine, Algeria
- 1 Department of Computer Science, Normal High School of Constantine, Constantine, Algeria
- 2
- 3
Journal of Software Engineering and Applications·Volume 06 (2013)·Pages 147–155·Published 29 March 2013·DOI10.4236/jsea.2013.63019
Copy link · social · email
Abstract
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.
KeywordsAADLTimed AutomataTransformationVerificationUppaal
- R. Lammel, J. Saraiva and J. Visser, “Generative and Transformational Techniques in Software Engineering,” Lecture Notes in Computer Science, Vol. 4143, 2006, pp 36-64. doi:10.1007/ 11877028
- SAE International, “Architecture Analysis & Designe Language (AADL),” Standard Version 2, 2009.
- M. Chkouri, A. Robert, M. Bozga, J. Sifaksi, “Translating AADL into BIP-Application to the Verification or Real-Time Systems,” Proceedings of MODELSACES-MB-Model Based Architecting and Construction of Embedded Systems, 2008, pp. 5-19.
- R. Alur and D. L. Dill, “A Theory of Timed Automata,” Theoretical Computer Science, Vol. 126, No. 2, 1994, pp. 183-236. doi:10.1016/0304-3975(94)90010-8
- J. Bengtsson and W. Yi, “Timed Automata: Semantics, Algorithms and Tools,” Lecture Notes in Computer Science, Vol. 3098, 2004, pp. 87-124.
- K. G. Larsen, P. Pettersson and W. Yi, “Uppaal in a Nutshell,” International Journal on Software Tools for Technology Transfer, Vol. 1, 1997, pp. 134-152. doi:10.1007/s100090050010
- D. A. Olivero, S. Tripakis and S. Yovine, “The Tool KRONOS Hybrid Systems III: Verification and Control,” Lecture Notes in Computer Science, Vol. 1066, 1996, pp. 208-219.
- D. Steinberg, F. Budinsky, M. Paternostro and E. Merks, “Eclipse Modeling Framework-Chapter Ecore Modeling Concepts,” 2nd Edition, Addison-Wesley, Boston, 2008.
- M. E. Hamdane and A. Chaoui, “Specification and Verification of Timed Automaton Using Meta-Modeling and Graph Grammars,” Proceedings of the 4th IEEE International Conference on the Applications of Digital Information and Web Technologies, Stevens Point, 2011, pp. 137-142.
- F. Jouault and I. Kurtev, “On the Architectural Alignment of ATL and QVT,” ACM Symposium on Applied Computing (SAC’06), 2006.
- F. Jouault and I. Kurtev, “On the Architectural Alignment of ATL and QVT,” Proceedings of the SAC’06 ACM Symposium on Applied Computing, 2006, pp.1188-1195.
- Xpand Documentation, 2010. http://ditec.um.es/ssdd/xpand_reference.pdf
- T. Vergnaud, “Modélisation des Systèmes Temps-Réel Répartis Embarqués pour la Génération Automatique d’Applications Formellement Vérifiées,” Ph.D. Thesis, école Nationale Supérieure des Télécommunications, 2006.
- L. Pi, J. P. Bodeveix, M. Filali and M. K. Dianfum, “A Comparative Study of FIACRE and TASM to Define AADL Real Time Concepts,” Proceedings of the 14th IEEE International Conference on Engineering of Complex Computer Systems, Potsdam, 2-4 June 2009, pp. 347-352.