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

• 作者: 李振松 顾斌
• 来源期刊: 计算机科学
• 学科: 工学
• 关键词: AADL 行为模型 模型转换 UPPAAL 验证
• 年，卷（期）: 2012,（2）
• 所属期刊栏目: 软件工程
• 页码范围: 159-161,169
• 分类号: TP302
• 字数: 3585字
• 语种: 中文
• DOI: 10.3969/j.issn.1002-137X.2012.02.037

摘要

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

作者信息

序号	姓名	单位	发文数	被引次数	H指数	G指数
1	顾斌		19	85	6.0	8.0
2	李振松		8	28	3.0	5.0