JSEA  Vol.5 No.12 B , December 2012
Formal Modeling and Analysis of AADL Threads in Real Time Maude
ABSTRACT
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.

Cite this paper
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. 12, 2012, pp. 187-192. doi: 10.4236/jsea.2012.512B036.
References
[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.

 
 
Top