期刊名称：Journal of Software Engineering and Applications
印刷版ISSN：1945-3116
电子版ISSN：1945-3124
出版年度：2012
卷号：5
期号：12B
页码：187-192
DOI：10.4236/jsea.2012.512B036
出版社：Scientific Research Publishing
摘要：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.
关键词：Architecture Description Language (ADL); AADL thread component; Real Time Maude; Model Checking
