基于UPPAAL的AADL行为模型验证方法研究

摘要：

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

关键词：AADL、行为模型、模型转换、UPPAAL、验证

所属期刊栏目：39

分类号：TP302(计算技术、计算机技术)

资助基金：国家自然科学基金重大研究计划项目90818024

在线出版日期：2012-04-27（万方平台首次上网日期，不代表论文的发表时间）

页数：共4页

页码：159-161,169