Formal Modeling and Analysis of AADL Threads in Real Time Maude


This paper presents, without altering the AADL meta-model, a formal description of static and behavioral aspects of the AADL thread component. This active and concurrent applicative component of AADL poses many challenges to its formalization and analysis including instantaneous and/or delayed communications, concurrent tasks and time-dependent features, and the need to analyze correctness. This formalization, based on real-time object-oriented theories, allows not only a precise description of the semantics of threads composition with respect to their timing requirements but also makes possible the formal verification of behavioral properties.

Share and Cite:

F. Belala, M. Benammar, K. Barkaoui and A. Hicheur, "Formal Modeling and Analysis of AADL Threads in Real Time Maude," Journal of Software Engineering and Applications, Vol. 5 No. 12B, 2012, pp. 187-192. doi: 10.4236/jsea.2012.512B036.

Conflicts of Interest

The authors declare no conflicts of interest.


[1] C. Jerad, K. Barkaoui, and A. Grissa-Touzi, ‘Hierarchical Verification in Maude of LfP Software Architectures’, In ECSA'07, 1st European Conference on Software Architecture, Aranjuez (Madrid), LNCS , Springer, 2007, pp. 156-170.
[2] SAE International, “Architecture Analysis and Design Language (AADL) Standard”, Version 2, SAE Dtaft Standard AS5506 V2, 2008.
[3] M. Benammar, F. Belala, , K. Barkaoui, and N. Benlahrache, “Extension d’ABAReL par les Propriétés d’Exécution”, CAL’09, 3ième Conférence Francophone Sur les Architectures Logicielles, Cépaduès-Editions, RNTI L-4,2009, pp.45-58.
[4] P. C. ?lveczky, “Real-Time Maude 2.3 Manual”, Department of Informatics, University of Oslo, 2007.
[5] 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, 2004, pp. 2741-2756.
[6] Z. Yang, K. Hu, D. Ma, and L. Pi, “Towards a Formal Semantics for The AADL Behavior Annex”, In Design, Automation & Test in Europe DATE 2009, pp. 1166-1171.
[7] M. Chkouri, A. Robert, M. Bozga, and J. Sifakis, “Translating AADL into BIP -Application to the Verification of Real-time Systems”, In Proc. of MoDELSACES-MB Model Based Architecting and Construction of Embedded Systems, 2008, pp. 39-54.
[8] O. Sokolsky, I. Lee, and D. Clarke, “Process-Algebraic Interpretation of AADL Models”, 14th International Conference on Reliable Software Technologies, LNCS 5570, 2009, pp. 222-236.
[9] D. Monteverde, A. Olivero, S. Yovine, and V. Braberman, “VTS-based Specification and Verification of Behavioral Properties of AADL Models”, Verimag Research Report n° TR-2008-11, 2008.
[10] J. Meseguer, “Membership algebra as a logical framework for equational specification”, Recent Trends in Algebraic Development Techniques, LNCS, Springer Berlin/Heidelberg, Volume 1376, 1998, pp. 18-61.
[11] M. Clavel, F. Duran, S. Eker, N. Marti-Oliet, P. Lincoln, J. Meseguer, and C. Talcott, Maude Manual (Version 2.4), 2008.
[12] P. Dissaux, J.P. Bodeveix, M. Filali, P. Gaufillet, and F. Vernadat, “AADL Behavioral Annex”, Pro. of the DASIA’06, Data Systems In Aerospace- Conference, Berlin, Germany, ESA SP-63, 2006.
[13] P. Gaufillet, “TOPCASED-Toolkit In Open source for Critical Applications & systems Development”, AADL Workshop, 2005.

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.