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

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.

Share and Cite:

M. Hamdane, A. Chaoui and M. Strecker, "Toolchain Based on MDE for the Transformation of AADL Models to Timed Automata Models," Journal of Software Engineering and Applications, Vol. 6 No. 3, 2013, pp. 147-155. doi: 10.4236/jsea.2013.63019.

Conflicts of Interest

The authors declare no conflicts of interest.

References

[1] 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
[2] SAE International, “Architecture Analysis & Designe Language (AADL),” Standard Version 2, 2009.
[3] 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.
[4] 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
[5] J. Bengtsson and W. Yi, “Timed Automata: Semantics, Algorithms and Tools,” Lecture Notes in Computer Science, Vol. 3098, 2004, pp. 87-124.
[6] 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
[7] 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.
[8] D. Steinberg, F. Budinsky, M. Paternostro and E. Merks, “Eclipse Modeling Framework-Chapter Ecore Modeling Concepts,” 2nd Edition, Addison-Wesley, Boston, 2008.
[9] 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.
[10] F. Jouault and I. Kurtev, “On the Architectural Alignment of ATL and QVT,” ACM Symposium on Applied Computing (SAC’06), 2006.
[11] 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.
[12] Xpand Documentation, 2010. http://ditec.um.es/ssdd/xpand_reference.pdf
[13] 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.
[14] 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.
[15] B. Berthomieu, P.-O. Ribet and F. Vernadat, “The Tool TINA Construction of Abstract State Spaces for Petri Nets and Time Petri Nets,” International Journal of Production Research, Vol. 42, No. 14, 2004, pp. 2741-2756. doi:10.1080/00207540412331312688
[16] P. E. Hladik , F. Peres and X. Shi, “Analyse d’Un Modèle AADL à l’Aide de Pola,” Proceedings of AFADL’2010, Approches Formelles dans l’Assistance au Développement de Logiciels, Poitiers, 2010, pp. 239-243.
[17] Y. Zhang, Y. Dong, Y. Zhang and W. Zhou, “A Study of the AADL Mode Based on Timed Automata,” Proceedings of the 2nd IEEE International Conference on Software Engineering and Service Science, Beijing, 15-17 July 2011, pp. 224-227.

Copyright © 2024 by authors and Scientific Research Publishing Inc.

Creative Commons License

This work and the related PDF file are licensed under a Creative Commons Attribution 4.0 International License.