Abstract: 为了实现AADL(体系结构分析与设计语言)行为模型的分析验证，基于行为附件的文法结构以及行为描述 方式，提出了AADL行为模型与UPPAAL下时间自动机模型之间的模型转换规则。在转换规则的基础上，设计和实 现了自动转换的原型工具。最后以航天器控制系统中制导、导航与控制计算机从陀螺取数的AADL模型为例，经自 动转换得到时间自动机模型，并在UPPAA工下仿真、验证其行为正确性，同时证明了模型转换的有效性。

Key words: AADL, Behavior model, Model transformation, UPPAAI，Verify