The configuration information correctness of the integrated modular avionics (IM A) system is an important guarantee of operational reliability. Reconfiguration of configuration information provides conveniences for system updating and transplantation， and brings unsafe factors to system. Concerning the detection method for the correctness of the IMA system which satisfies ARINC653 specification, the transformation and analysis of the architecture analysis and design language (AADL) model are researched. Elements mapping rules from ARINC653 system configuration information to the AADL model are proposed, including module, partition, proce ss, health, monitoring, communication and other core concepts. A model transform ation approach is given, and a formal semantic verification of the configuration information correctness of AADL model is presented based on a third-party tool. Finally, an example analysis is provided.