Share This Article:

Formal Modeling and Analysis of AADL Threads in Real Time Maude

Full-Text HTML Download Download as PDF (Size:288KB) PP. 187-192
DOI: 10.4236/jsea.2012.512B036    3,275 Downloads   4,543 Views Citations


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. 12B, 2012, pp. 187-192. doi: 10.4236/jsea.2012.512B036.

Copyright © 2019 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.