Research ArticleOpen AccessGoogle Scholar indexed
Formal Modeling and Analysis of AADL Threads in Real Time Maude
Department of Computer Science, Mentouri University, Constantine, Algeria
Department of Computer Science, Mentouri University, Constantine, Algeria
CEDRIC, Conservatoire National des Arts et Métiers, Paris, France
CEDRIC, Conservatoire National des Arts et Métiers, Paris, France
- 1 Department of Computer Science, Mentouri University, Constantine, Algeria
- 2 Department of Computer Science, Mentouri University, Constantine, Algeria
- 3 CEDRIC, Conservatoire National des Arts et Métiers, Paris, France
- 4 CEDRIC, Conservatoire National des Arts et Métiers, Paris, France
Journal of Software Engineering and Applications·Volume 05 (2013)·Pages 187–192·Published 17 January 2013·DOI10.4236/jsea.2012.512B036
Copy link · social · email
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.
KeywordsArchitecture Description Language (ADL)AADL thread componentReal Time MaudeModel Checking
- 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.
- SAE International, “Architecture Analysis and Design Language (AADL) Standard”, Version 2, SAE Dtaft Standard AS5506 V2, 2008.
- 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.
- P. C. ?lveczky, “Real-Time Maude 2.3 Manual”, Department of Informatics, University of Oslo, 2007.
- 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.
- 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.
- 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.
- 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.
- 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.
- 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.
- M. Clavel, F. Duran, S. Eker, N. Marti-Oliet, P. Lincoln, J. Meseguer, and C. Talcott, Maude Manual (Version 2.4), 2008.
- 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.
- P. Gaufillet, “TOPCASED-Toolkit In Open source for Critical Applications & systems Development”, AADL Workshop, 2005.