A Journal of Software Engineering and Applications, 2012, 5, 187-192
doi:10.4236/jsea.2012.512b036 Published Online December 2012 (http://www.scirp.org/journal/jsea)
Formal Modeling and Analysis of AADL Threads in Real
Time Maude
F. Belala1, M. Benammar1, K. Barkaoui2, A. Hicheur2
1Department of Computer Science, Mentouri University, Constantine, Algeria; 2CEDRIC, Co nservatoire National des Arts et Métiers,
Paris, France.
Keywords: Architecture Descri ption Language (A DL), AADL thread component, Real Time Maude, Model Checking.
Received 2012
ABSTRACT
This pap er presents, without a lterin g the AAD L meta -model, a formal description o f 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- depen-
dent features, and the need to analyze correctness. This formalization, based on real-time object-oriented theories, al-
lows not only a p recise description of the se mantics of threads composition with respect to their timing requ i reme nts but
also makes po ssible the formal verifica tion of behavioral properties.
1. Introduction
The problem of ensuring as early as possible the cor-
rectness of a software architecture (SA) is of great im-
portance in the develop ment life-cycle of software prod-
ucts. Recently, model checking, that is completely auto-
matic, allows developers to perform exhaustive verifica-
tion of the SA (as for e.g. [1]). In this pap er, we will use
this technique to assess whether an SA specification
noted in AADL language satisfies desired architectural
properties.
The architecture description language AADL (Archi-
tecture Analysis and Design Language) [2] is a formal
notation for describing the architectural plan of real time
embedded system at various abstraction levels. It offers
the capacity to assembly both information concer ni ng t he
application structure and its deployment.
However, AADL is focused on the architectural as-
pects of the system components and their connections,
but doesn’t deal directly with their behavioral aspects.
Thus, the formal reasoning on AADL architecture or its
formal analysis poses a set of challenges, including: 1)
Modeling concurrent and distributed components of
AADL architecture, 2) Modeling components communi-
cation with transmission delays, 3) Modeling
time-dependent behaviors, and 4) Analyzing behavior
properties with respect of AADL declared constraints.
Several works are being done in literature tempting to
formalize AADL architectural description while trans-
forming it to o ther formal mode ls. These models are pro-
vided on the basis of some well known formalisms such
as, timed automaton, timed Petri nets (TPN), real time
process algebra (ACSR) or timed abstract state machine
(TASM), that come with some convenient tools (TINA
[5], CADP [6], etc.). Others more practical works are
also raised; a translation from VTS (Visual Timed event
Scenarios) to Time Petri Nets in [9] enables the mod-
el-checking of properties expressed in VTS over AADL
models using TPN-based tools. Nevertheless, most of
these co ntributions have focused on detecting deadlocks
states or on concurrent access control to shared data, they
have been interested by formalization of only some
AADL concepts.
This paper shows how we can met all the cited chal-
lenges by extending the semantic framework ABAReL
annex proposed in [2] and based on rewriting logic. Our
extension consists in defining the behavior specification
of the fundamental concurrent AADL execution unit
Thread as a real-time re write theory
ℜ
T = (ΣT, ET, LT, RT).
The membership equational theory (ΣT, ET) describes all
declared elements in the AADL thread description (flo ws,
properties, etc.). The labeled rewrite rules (LT, RT), in-
stantaneous and tick ones, describe the thread behavior
according to its configurations evolution, taking into
account its local states and those of its connection ports,
as well as its declared timing requirements. In addition,
proof of generic and crucial architectural properties (such

Formal Modeling and Analysis of AADLThreads in Real Time Maude
188
as safety and liveness) is successfully achieved via the
RT-Maude model-checker.
Real-Time Maude [4] extends the rewriting logic tool
Maude to support formal specification and analysis of
object based real-time systems which are suitable for
modeling AADL architectural system. The high-per-
formance RT-Maude tool provides a range of analysis
techn ique s, i nclud ing t ime -bounded linear temporal lo gic
model checking, being used in our study.
The remainder of this paper is organized as follows.
Section 2 introduces basic concepts of both Real-Time
Maude language and AADL notations. In section 3, we
show how we enrich ABAReL annex to formal specify,
simulate and further analyze AADL architecture with
several communicating threads. A case study is given in
section 4 to illustrate and validate the feasibility of our
approach. Finally, we conclude by a synthesis of
achieved work and related prospects to its continuation.
2. Basic Concepts
2.1. RT-Maude Overview
Rewriting Logic [10] has many operational environments
implementin g its theoretical concepts, the most kno wn is
the Maude syste m [11]. T he obje ctive of this section is to
present essential concepts of RT-Maude [4], an extension
of Maude language appropriate to model and analyze
object o riented real time syste ms.
A RT-Maude module implements real-time rewrite
theory ℜ which is a quadruplet of the form [Σ, E, (L,
R), (L’, R’)], where (Σ, E) is a membership equational
logic theor y, the signat ure Σ and conditional equations E
describe system states as an algebraic data type. It must
include a special sort Time modeling a time domain
(dense or discrete). L are labels o f the c onditional instan-
taneous rewrite rules R. Each re write rule is noted crl [l]:
[t] → [t'] if cond and models the possible instantaneous
local transition betwee n states of the concurr ent real-time
system. [t], [t'] and cond are equivalence classes of al-
gebraic terms belonging to the set TΣ,E(X). L’ is another
labels set for tick rewrite rules R’ written with a particu-
lar syntax crl [l’] : {t} => {t`} in time D if cond. They
model the advance of a time D in the system of state t if a
condition cond is checked. D of sort Time denotes the
duration of the rewrite. {_} is a free constructor of sort
GlobalSystem.
The syntax of RT-Maude modules supports ob-
ject-oriented concepts as objects, messages, classes, and
multiple class inheritance. A real-time system state in
this case is modeled by a multiset of objects and juxta-
posed messages, usually called a configuration, it is a
term of the built-in sort Configuration. Concurrent inte-
ractions between the objects are governed by rewrite
rules. An object is an instance of class. It is possible to
declare subclasses and profit from the heritance concept.
The messages are declared using the key word msg. The
dynamic behavior of concurrent object systems is axi-
omatized by specifying each of its concurrent transition
patterns as a rewrite rule.
RT-Maude offers a variety of analysis tools. Among
them the linear temporal logic Maude model checker
used in our case study, it checks whether each behavior
“up to a certain time,” as explained previously, satisfies a
temporal logic formula. Entries of this tool are the sys-
tem behaviour specification (as RT-Maude modules) and
the properties that we want to state and prove about this
system. The output result is a positive answer if the
property is satisfied, and one counterexample should the
opposite occurs.
2.2. Overview of the AADL Language
AADL (Architecture Analysis and Design Language) is
devoted to real time embedded systems description [2]. I t
describes software applications, their execution plat-
forms and how components are composed and interact to
form complete system architectures. It also describes
component functional interfaces, component connections
and how software components are allocated to hardware
ones.
The abstract declaration of AADL component contains
component type and one or more implementatio n s. The
component type declaration specifies functio nal interface
in terms of features, flow, and properties. A component
implementation specifies its inter nal str uctur e in ter ms of
subcomponents, connections betwee n t he sub c o mponent s
features, flows across a sequence of subcomponents,
modes to repr esent operational states, and properties.
AADL offers thread component like schedulable units
for the concurrent execution, processes to represent
spaces of virtual addresses, and systems to support the
hierarchical organization of both threads and processes.
AADL also allows the execution platform (or hardware
components) modelling in terms of proc essors (support-
ing the execution of threads), memory for the data and
code storage, and bus to represent the physical intercon-
nection. AADL properties are the key concept of this
langua ge. T hey desc ribe throu gh its o wn notati ons, s ome
constraints on the architectural elements, components,
subcomponents, interface elements, connections, etc.
For each component, one can associate properties and
give them values .
In order to integrate the academic research results in
the industrial development process, AADL has some
recent tools developed within the European project
framework ASSERT (Automated proof-based System

Formal Modeling and Analysis of AADLThreads in Real Time Maude
189
Software Engineering for Real-Time systems) [13].
However, the AADL standard uses a restricted formal
model based on operational mode and its corresponding
transitions rules to express the commutation between
system execution configurations representing the behav-
iour of a system.
We are mainly interested in this paper by giving a
formal setting for the AAD L component thread, in order
to define both its structure and behavio ur and a lso to give
a mathematical semantic for its execution model.
3. The Real-Time Maude Specification of
AADL Threads
Traditionally the AADL standard defines simplified au-
tomata based semantics for threads (figure 1). A thread
can be stopped, inactive, or in activity. An active thread
can be waiting for dispatch, computing (Compute state),
or blocked on resource access. Only active threads ex-
ecute their instructions. The standard gives also the pos-
sibility of specifying the implementation conditions of
the threads by the declaration of some properties (dead-
line, dispatch protocol, period, etc).
The complex task of a thread carried out at the Com-
pute state (figure 1), consists in data (and/or events) re-
ceipt, computation and signals data (and/or event) send.
Particularly, the hierarchical Compute state of this
automaton is composed of others substates (figure 2).
Ho wever, this e xec utio n se mant ics o f AAD L thr ead do es
not appear at the architecture description level. Only
possible modes and their execution properties are de-
clared. Our work aims to extend the behavioral annex
(ABAReL for AADL Behavioral Annex based on Re-
writing Logic) to define behavioral aspects of an AADL
threads composition without altering the AADL me-
ta-model.
St a rt
Halted
Threadinit
AwaitMode
ThreadActivate
AwaitDispatch
Thread
Deactivate
Thread
Finalize
complete
complete
complete
complete
initDeadline
Compute
Figure 1 . The state-transition model of AADL thread.
3.1. Modeling AADL Thread
We associate to an AADL thread component T, a for ma l
mathematical model, represented by a Real-Time re write
theory RT = (ΣT, ET, LT, RT), where (ΣT, ET) is a member
recover
Ready
Clock-P
Running
Clock-C
Awaiting-resource
Clock-P
Compute-State
resume
preempt
Block on
Release
Unblock
on Release
Complete
Figure 2 . Compute state of a Thread.
ship equational theory describing the thread static struc-
ture. The ΣT signature specifies the sorts (and subsorts)
set and mainly the operators set necessary to describe
each clause of thread description: features, properties,
modes, type and implem entation . Op erators considered in
ΣT may free ze the rewriting under their specified argu-
ments. The instantaneous and tick rewrite rules RT (la-
beled by LT set elements) describe the behavior of thread
dynamic configurations, involving, at each stage, local
state of a thread and the state of each one of its connec-
tions ports.
As RT-Maude language implements real time rewrite
theories, we use it to build the appropriate RT-Maude
executable modules. We define a set of generic rules
(table 1) mapping each architectural element involved in
an AADL architecture description to RT-Maude con-
cepts. As shown in Table 1, an AADL architecture de-
scription is mapped to RT-Maude module which may
contain many threads declaration (thread class). Thus,
formal analysis of behavioral properties with respect of
AADL thread declared constraints is defined very natu-
rally.
Table 1. Mapping AADL architectural elements to RT-
Maude object-oriented concepts.
AADL Arch itectural
Element RT-Maude Object-Oriented Concepts
AADL Ar chitecture
Real-Time object-oriented rewrite
theory
Thread component
Thread class
Component Interface
PortState sort for IPort and
OPort attributes, File sort for Ac-
cessData, InBufferPort and OutBuffer-
Port
attributes
Thread State
ThreadState sort
Thread Configuration
Conditional rewrite rules
Thread Interac tion
Message Transmission
between objects
(instances of thread
class)
Flow Latency in a
Thread Message transmission time
Thread Implementation
ThreadImpl class (subclass of class
Thread)
Thread execution
properties Time sort for Period and Execution-time
attributes

Formal Modeling and Analysis of AADLThreads in Real Time Maude
190
In this more abstract level of f o r malization, thread type is
modeled by the Thread class (figure 3), whose attributes
are respectively: 1) the functional interfaces IPort and
OPort , 2) data subcomponent, represented as a buffer,
related to each connection port InBufferPort, OutBuffer-
Port and 3) TState to specify its state. The PortState
sort represents the functional interfaces states of a thread.
Its internal structure (or its implementation) is specified
by the ThreadImpl class (figure 3) having the attributes:
1) S sta te specify substate of the “Compute” composite
state, 2) Time (predefined sort) specify both temporal
execution properties (Period and Execution-Time ) and
the Clock-P and Clock- C clocks for the warning of the
thread period and execution time. It is obvious that the
ThreadImpl class is declared as a subclass of the Thread
class and profits fro m the inheritance concept.
class Thread | IPort : PortState, OPort : PortState,
TState : ThreadState, InBufferPort : File, AccessData :
File, OutBufferPort : File, MaxPreempt : Nat, MaxData :
Nat, NBS : Set .
class ThreadImpl | Substate : Sstate, Period :
Time,Execution-time : Ti me, C lock-P : Time, Clock-C :
Time .
subclass ThreadImpl < Thread .
subsort Sstate < ThreadState .
Figure 3 . RT-Maude specification of AADL thread。
We define the passage of data (and/or event) flow
through a threads connection as a messages transmission
between a thread and its neighbors (threads). Message
transmission time is taken into account by the DlyMsg
sort modeling the flow latency time.
3.2. Defining AADL Architecture in RT Maude
Since in AADL architecture description of a system, the
thread is never alone, we have to model thread behaviour
inside a larger configuration containing some intercon-
nected threads with the passage of data flow (the mes-
sage transmission). Besides, the thread temporal execu-
tion properties (Period and Compute-Execution-Time)
have also to be considered. Indeed, we first define with
constructor operator s, the thread states (wait or compute),
the thread substat es ( Ready, Running, Awaiting-Resource,
Complete and noSub) and the port states (waitIn , waitOut,
receive and send). Then, the behaviour formalization
aspect starts with the sp ecific ation of the visible changes
of the thread states, associated to its connec ti on p o r ts a nd
materialized by the rewrite rules Data-Receive and
Data-send (see figure4) . The Data-Receive rule prepares
thread for a new execution period, after receiving a
message. It changes the thread state from wait to
compute and its substate from noSub to Ready initializ-
ing the clocks by the values, specified in the execution
properties. The Data-Send rule putts the thread in its
initial state after a period elapse and an execution time. It
transforms the thread state from compute to wait and its
substa te from Complete to noSub and then, genera tes the
message with the thread execution result for the trans-
mission.
rl[Data-Receive]:(from T1 to T2 transfer DT) < T2:
ThreadImpl | IPort: waitIn, TState : wait, Substate:
noSub , Clock-P: 0, Clock-C: 0, Period: R, Execu-
tion-time: R', InBufferPort: L2 >
=>
< T2 : ThreadImpl | IPort: receive, TState:
compute , Substate: Ready, Period: R,Execution-time:
R', Clock-P: R, Clock-C: R', MaxData: 0, MaxPreempt:
0, InBufferPort: DT; L2 >.
rl[Data-Send]: < T1: ThreadImpl | OPort: waitOut,
TState: compute, Substate: Complete, OutBufferPort:
L; DT, NBS:(T2 & R), Clock-P: R1, Clock-
C: R2,
MaxPreempt: N, MaxData: N1 >
=> < T1: ThreadImpl | OPort: waitOut, TState: wait ,
Substate: noSub, OutBufferPort: L , NBS: T2 & R ,
Clock-P: 0, Clock-C: 0, MaxPreempt: 0, MaxData: 0 >
dly(from T1 to T2 transfer DT, R).
Figure 4. Specification of AADL connection and interac-
tion.
In this formalization, we take into account the substate
of the thread in its active hierarchical state compute. We
define these substa tes a nd the ir co rrespo nding tr ansitions
(see figure 2) and also the corresponding declared prop-
erties. The first rewrite rule, in figure 5, changes the
thread substate from Ready to Running and prepares the
received data treatment. The rewrite rule fin ish considers
the particular case, where the thread doesn’t have an out
port (OPort = NoPort). It gives the thread in its initial
state after elapse of the period time. The conditional re-
write rule s resume, preempt, block-on-Release-Re s ource,
Unblock-on-Release-Resource, recover and complete-rec
define the transitions between substates of the compute
state. The function mte is used to calculate the maximal
time elapse of a thread configuration, before a significant
action is taken (about the minimum values of the two
clocks). Moreover, the function delta models the effect
of passage of a time R on the thread by decreasing one or
both of its clocks according to the time elapsed. These
two functions are used in the tick rule in order to
calculate and apply the time elapse on the thread
confi gur atio n (fi gur e 6). The nonexec attribute o f the tick
rule indicates that th is rule advances time whe n no o ther
rule is executable. The delta operation modifies only the
attributes of sort time . The equations calculate the delta
operation effect on thread configuration and on the mes-
sages transmission. The mte operation evaluation con-
siders a thread (if it is at compute state) with its clocks
initialized by the execution properties values. Then, it
considers the distribution of the mte operation on the
configuration.

Formal Modeling and Analysis of AADLThreads in Real Time Maude
191
Crl [init] : < Imp : ThreadImpl |InBufferPort: L,
AccessData: EmptyFile, Substate: Ready, Clock-C: R'>
=> < Imp: ThreadImpl | InBufferPort: Queu(L),
AccessData: Head(L), Substate: Running, Clock-C: R' >
if (R' > 0) .
crl [complete-Rec] : < Imp: ThreadImpl | IPort :
receive , TState : compute, Substate: subS ,
AccessData: Temp2 , OutBufferPort: L, OPort: waitOut,
Clock-P: R, Clock-C : R' >
=> < Imp: ThreadImpl | IPort: waitIn , TState: compute,
AccessData: EmptyFile , OutBufferPort: Temp2 ; L ,
Substate: Complete, OPort : waitOut , Clock-P : R,
Clock-C : R' > if (R == 0) .
rl[finish]: <Imp : ThreadImpl | IPort: receive, TState:
compute, Substate: Complete , OPort: NoPort, Clock-P:
R, Clock-C: R', MaxPreempt: N, MaxData: N1 > => < Imp:
ThreadImpl | IPort: waitIn, TState: wait, Substate:
noSub, OPort: NoPort, Clock-P: 0, Clock-C: 0,
MaxPreempt: 0, MaxData : 0 > .
Figure 5. Specification of AADL thread Behaviour.
Tick rule
crl [tick] : {C:Configuration}
=> {delta(C:Configuration, R)} in time R
if (R <= mte(C:Configuration)) /\(not
agerEnabled(C:Configuration)) [nonexec] .
delta
operation
eq delta(< Imp : ThreadImpl | Substate :
Running, Clock-P : R , Clock-C : R' >, R'')
= < Imp : ThreadImpl | Substate : Running,
Clock-P : R monus R'' , Clock-C : R' monus
R'' > .
mte
operation
ceq mte(NeC NeC') = min(mte(NeC),
mte(NeC')) if (NeC =/= none) /\
(NeC' =/=
none) .
Figure 6. The elapsed time on thre ad configuration.
4. Formal Analysis of Thread Properties
The concurrent execution of several threads and the ef-
fect of interactions between them are defined by this
ABAReL annex extension of AADL. This section will
explain how, under appropriate assumptions, we can
model check in RT-Maude behaviour properties AADL
architectural system specified as an object-oriented
real-time module.
ops GPS TGPS TSCREEN : -> Oid [ctor] .
op initState : -> GlobalSystem .
eq initState = {(from GPS to TGPS transfer data1 ) < TGPS:
ThreadImpl |IPort : waitIn, T State : wait, Substate :
noSub , OPort : waitOut, InBufferPort : EmptyFile,
AccessData : EmptyFile, OutBufferPort : EmptyFile,
Period : 20, Execution-time : 10, Clock-P : 0, Clock-C :
0, MaxData : 0, MaxPreempt : 0 , NBS : (T SCREEN & 4) >
< TSCREEN : ThreadImpl | IPort : waitIn, TState : wait,
Substate: noSub, OPort: NoPort, InBufferPort :
EmptyFile, AccessData : EmptyFile, OutBufferPort :
EmptyFile , Period : 15, Exec ution-time : 7, Clock-P:
0, Clock-C: 0, MaxData : 0, MaxPreempt: 0 , NBS : EmptySet
>}.
Figure 7 . The GPS example in RT-Ma ude.
We will deal here with properties such as reachability,
safety and liveness through the modeling of a GPS sys-
tem as case study.
We consider an AADL architectural description mod-
eling a GP S syst em example. T his sys te m sho uld disp la y
the current position information for the user. It is com-
posed of one sensor GPS and two threads: TGP S and
TScreen. The GPS sensor captures information parame-
ters from satellite a nd send s the m to thr ead TGPS. TGPS
reads these parameters, converts them into an internal
representation, and sends the result to thread TScreen.
This one displays the recent position received periodi-
cally. The AADL specification give s only stat ic descrip-
tion of components and their connections including, for
each thread description, the specification of implementa-
tion condition s. This is done b y the properties declaration,
such as: Dispatch -Protocol, Period and Compute-Ex-
ecution -Time a nd their various values.
Giving AADL description, we can exploit the ex-
tended ABAReL annex to formalize the behavior of each
declared thread TGPS or TScreen and their possible
connection. For this case, we associate an RT-Maude
module to each thread, specifying its static and dy-
namic aspects. In order to provide the global system be-
havior specification, we extend the obtained modules by
additional information defining communication between
connected threads (TGPS and TScreen). A code portion
of this global RT-Maude module is shown in figure 7.
Each thread name is declared as an object identifier. In-
itstate oper ator gives for e ach thread its i nitial co nfigura-
tion thanks to the equation clause. Each thread in com-
pute state must have the following substates: Ready,
Running and Awaiting-Resource. In this case, we can
check for instance the following properties. (P1) The
final state (Complete substate) of the thread execution
process can be reached in time. (P2)
The thread in execution (compute state) is never (i)
preempted infinitely, (ii) waiting resource infinitely. (P3)
The thread will be eventually executed (running subs-
tate), respecting the execution time declared in Com-
pute-Execution-Time property. The core module MOD-
EL-CHECK-AADL-PROP (figure 8) impo rts the predefined
module TIMED -MODEL -CHECKER and the module
AADL-SPEC to be analyzed. The specification of the
previous properties is made through the atomic proposi-
tions: CompleteS ta te TGPS (P1), CompleteStateT-
SCREEN (P2) and RunningState (P3). The check, for
instance, of t he property (P1) by the LTL model-checker
of RT-Maude is launched by this command: (mcinitS-
tate1|=t(<>completeStateTGPS)/\(<> CompleteSta-
teTSCREEN) in time <= 70 .)

Formal Modeling and Analysis of AADLThreads in Real Time Maude
192
(tomod MODEL-CHECK-AADL-PROP is
including TIMED-MODEL-CHECKER .
protecting AADL-SPEC .
ops RunningState CompleteStateTGPS
CompleteStateTSCREEN : -> Prop [ctor].
var REST : Configuration .
var Imp : Oid . vars R R' R'' : Time .
eq {REST <TGPS:ThreadImpl|Substate: Complete>}
|= CompleteStateTGPS = true .
eq {REST < TSCREEN : ThreadImpl | Substate :
Complete >} |= CompleteStateTSCREEN =
true.
eq {REST < Imp : ThreadImpl| TState : compute,
Substate : Running >} |= RunningState = true.
endtom)
Figure 8. The MODEL-CHECK-AADL-PROP RT-Maude
module.
A direct and naive execution of this command returns
a counterexample indicating that the property (P1) is not
satisfied. To overcome this incorrect behavior, we asso-
ciate a time interval to t he preempt tr a nsition, so it can be
executed no more that a given time. The second suc-
cessful solution is to add priorities to some rewrite rules
execution. The screen shot of figure 9 shows that the
property (P1) is then evaluated to true in this case. In a
similar way, we check t he property (P2) and (P3).
Figure 9. Model-check AADL properties.
5. Conclusion
The proposed extension of behavioral annex ABAReL
based on object-oriented real-time rewrite theories is a
suitable semantic framework for AADL thread behavior
descriptio n. In this paper, we have exploited this formal
setting to define and analyze semantic execution model
of AADL architectural system, composed of intercon-
nected threads and juxtaposed messages under timing
require ments. Concurrent interactions between the ob-
jects are governed by ordinary rewrite rules correspond-
ing to instantaneous transitions and by “tick” rewrite
rules describing the time elapse . We showed how this
formalism supports the verification of thread temporal
execution properties via the LTL model checker tool of
RT-Maude system. In future, we will exploit the pro-
posed approach to analyze others properties of the
AADL standard, related to space and ti me partitioning.
REFERENCES
[1] C. Jerad , K. Barkao ui , an d A. Gri ssa-Tou zi, ‘Hi erarch ical
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épad uès-Editions,
RNTI L-4,2009, pp.45-58.
[4] P. C. Ölveczky, “Real-Time Maude 2.3 Manual”, De-
partment 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”, Internation al Journ al of Producti o n
Research, Vol. 42, 2004, pp. 27 41-2756.
[6] Z. Yang, K. Hu, D. Ma, and L. Pi, “Towards a Formal
Semantics for The AADL Behavior Annex”, In Design,
Autom ati o n & Te s t in Euro pe D ATE 20 09, 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
Constr uc tion of Embe d de d Sy s t e m s , 2008, pp. 39-54.
[8] O. Sokolsky, I. Lee, and D. Clarke, “Proces s-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,
“V TS-based S pecification an d Verificatio n 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 Tre nds in A lge brai c
Development Techniques, LNCS, Springer
Berlin/Heidelberg, Volume 1376, 1998, pp. 18-61.
[11] M. Clavel, F. Dura n, S. E ker, N . Marti-Olie t, P. L incoln, 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.