%0 Journal Article
%T 基于uppaal的aadl行为模型验证方法研究
%A 李振松
%A 顾斌？
%J 计算机科学
%D 2012
%X 为了实现aadl(体系结构分析与设计语言)行为模型的分析验证，基于行为附件的文法结构以及行为描述方式，提出了aadl行为模型与uppaal下时间自动机模型之间的模型转换规则。在转换规则的基础上，设计和实现了自动转换的原型工具。最后以航天器控制系统中制导、导航与控制计算机从陀螺取数的aadl模型为例，经自动转换得到时间自动机模型，并在uppaa工下仿真、验证其行为正确性，同时证明了模型转换的有效性。
%K aadl
%K 行为模型
%K 模型转换
%K uppaal
%K 验证
%U http://www.jsjkx.com/jsjkx/ch/reader/view_abstract.aspx?file_no=120237&flag=1