计算机科学 ›› 2012, Vol. 39 ›› Issue (2): 162-169.
• 软件工程 • 上一篇 下一篇
李振松,顾斌
出版日期:
发布日期:
基金资助:
LI Zhen-song GU Bin
Online:
Published:
摘要: 为了实现AADL(体系结构分析与设计语言)行为模型的分析验证,基于行为附件的文法结构以及行为描述 方式,提出了AADL行为模型与UPPAAL下时间自动机模型之间的模型转换规则。在转换规则的基础上,设计和实 现了自动转换的原型工具。最后以航天器控制系统中制导、导航与控制计算机从陀螺取数的AADL模型为例,经自 动转换得到时间自动机模型,并在UPPAA工下仿真、验证其行为正确性,同时证明了模型转换的有效性。
关键词: AADL,行为模型,模型转换,UPPAAL,验证
Abstract: 为了实现AADL(体系结构分析与设计语言)行为模型的分析验证,基于行为附件的文法结构以及行为描述 方式,提出了AADL行为模型与UPPAAL下时间自动机模型之间的模型转换规则。在转换规则的基础上,设计和实 现了自动转换的原型工具。最后以航天器控制系统中制导、导航与控制计算机从陀螺取数的AADL模型为例,经自 动转换得到时间自动机模型,并在UPPAA工下仿真、验证其行为正确性,同时证明了模型转换的有效性。
Key words: AADL, Behavior model, Model transformation, UPPAAI,Verify
李振松,顾斌. 基于UPPAAL的AADL行为模型验证方法研究[J]. 计算机科学, 2012, 39(2): 162-169. https://doi.org/
LI Zhen-song GU Bin. Research on Verification Method of AADI. Behavior Model Based on I1ppaal[J]. Computer Science, 2012, 39(2): 162-169. https://doi.org/
0 / / 推荐
导出引用管理器 EndNote|Reference Manager|ProCite|BibTeX|RefWorks
链接本文: https://www.jsjkx.com/CN/
https://www.jsjkx.com/CN/Y2012/V39/I2/162
Cited