R. Alur and D. Dill, A theory of timed automata, Theoretical Computer Science, vol.126, issue.1, p.183235, 1994.

B. Berthomieu, P. Ribet, F. Vernadat, and J. ,

J. Bernartt, J. Farines, M. Bodeveix, G. Filali, P. Padiou et al., Towards the verication of real-time systems in avionics: The Cotre approach, Eigth International workshop for industrial critical systems, pp.5-7, 2003.

J. Bodeveix, D. Chemouil, M. Filali, and M. Strecker, Towards formalizing AADL in proof assistants

R. Reussner and S. Shukla, Formal Foundations of Embedded software and componentbased softare architectures (ETAPS), pp.2-10, 2005.

A. Burns and A. Wellings, HRT-HOOD a structured design method for hard real-time Ada Systems, 1995.

E. Clarke, E. Emerson, and A. Sistla, Automatic verication of nite state concurrent system using temporal logic, ACM Transactions on Programming Languages and Systems, vol.8, issue.2, 1986.

P. Dissaux, AADL model transformation, DA-SIA, 2005.

P. Farail and P. Gaullet, Cotre as an AADL prole, Architecture Description Languages, p.167180, 2004.

P. H. Feiler, B. Lewis, and S. Vestal, The SAE architecture analysis & design language (AADL) standard: A basis for model-based architecturedriven embedded systems engineering, RTAS Workshop, p.110, 2003.

, MetaH User's Manual

, Honewell Technology Drive, 1998.