A study of the AADL mode based on timed automata

In order to solve the problem of real-time and correctness during the process of embedded software model testing, this paper put forward a testing method of embedded software based on AADL mode timed automata. Using AADL architecture model, this method generates a system component tree containing the mode information. By traversing this component tree breadth-firstly, the AADL mode timed automata is constructed. Meanwhile, we use UPPAAL, a tool for timed automata verification to verify the correctness and time property of this AADL model transformation method. Finally, this paper presents a case study on the verification of avionics flight control software to show the application scenario of this method.