We propose a verified transformation from a subset of AADL to TASM.
We give a reference semantics of the subset of AADL which is formalized in TTS.
We give a formal translational semantics of the subset of AADL by translating it to TASM.
We present a mechanized proof of the semantics preservation of the transformation from the subset of AADL to TASM.