Abstract: The rapid growth of software size and complexity has become an important challenge for designing and verifying modern high-quality UAV flight control software (FCS) system. Based on the architecture of Model Driven Engineering(MDE),an UAV flight control software model was established by using embedded real-time system modeling language( MAR I'E)，and an example of formal model for system dynamic behaviors based on timed automata was given.Considering the application background of UAV FCS system, we proposed a test case generation method based on timed automata, including establishment of testing architecture, coverage rules and strategics of test case generation. Lastly,a case study of timed automata modeling and test case generation for the main control module of an UAV FCS system were provided.

Key words: Model driven engineering,Model-based testing,Flight control software,timed automata,UAV system