Abstract: Architecture analysis and design language (AADL) is a standard and intuitive real-time system design tool, which provides uniform standards for key steps such as model design, analysis, verification, and automatic code generation. However, using simulation, the verification method of AADL model cannot obtain accurate results of end-to-end flow, especially for real-time systems with dynamic resource allocation. To solve this problem of inaccurate results, AADL is combined with the model checking method to traverse the systems infinite state space. Firstly, the AADL model of the real-time system is converted into a timed automata (TA) model, and the TA is used as the theoretical system for model checking verification. Secondly, the pattern of end-to-end delay requirements is defined, based on the demand classification of the response chain. Finally, the corresponding observer model is implemented according to the pattern and combined with the system model in parallel to reduce the time as well as space resources consumed by the verification algorithm.

Key words: real-time system verification, architecture analysis and design language (AADL), timed automata (TA), observer