Open AccessFormal Modeling and Analysis of AADL Threads in Real Time Maude
Author(s) -
Faïza Belala,
Malika Benammar,
Kamel Barkaoui,
A. Hicheur
Publication year - 2012
Publication title -
journal of software engineering and applications
Language(s) - English
Resource type - Journals
eISSN - 1945-3124
pISSN - 1945-3116
DOI - 10.4236/jsea.2012.512b036
Subject(s) - computer science , correctness , thread (computing) , programming language , component (thermodynamics) , object oriented programming , semantics (computer science) , formal verification , model checking , formal semantics (linguistics) , physics , thermodynamics
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