Verification and performance evaluation of AADL models