Formal Modeling and Analysis of AADL Threads in Real Time Maude

F. Belala, M. Benammar, K. Barkaoui, A. Hicheur

CEDRIC, Conservatoire National des Arts et Métiers, Paris, France.
Department of Computer Science, Mentouri University, Constantine, Algeria.

DOI: 10.4236/jsea.2012.512B036                

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.

Keywords

Architecture Description Language (ADL), AADL thread component, Real Time Maude, Model Checking

Conflicts of Interest

The authors declare no conflicts of interest.

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.