基于NuSMV的AADL行为模型验证的探究

• 作者: 刘博 李蜀瑜
• 来源期刊: 计算机技术与发展
• 学科: 工学
• 关键词: 嵌入式构件分析与设计语言 AADL集成开发环境 行为模型 NuSMV验证方法
• 年，卷（期）: 2012,（2）
• 所属期刊栏目: 智能、算法、系统工程
• 页码范围: 110-113
• 分类号: TP31
• 字数: 2765字
• 语种: 中文
• DOI: 10.3969/j.issn.1673-629X.2012.02.029

摘要

鉴于模型在软件系统开发中日趋重要的地位和AADL模型在嵌入式软件建模中的良好应用前景,为了在嵌入式软件系统开发前期保证AADL模型的质量,提出了一种基于模型测试的AADL架构和NuSMV模型的验证方法.文中首先对当前的AADL发展情况作简单介绍,然后对NuSMV验证模型的结构作大致分析,在随后的文章中对NuSMV的验证过程作详细的介绍.与此同时,使用具体的汽车巡航控制系统作为实例进行具体分析.文中通过测试用例执行输出进行验证来判断该方法的正确性.

作者信息

序号	姓名	单位	发文数	被引次数	H指数	G指数
1	李蜀瑜	陕西师范大学计算机科学学院	57	229	7.0	11.0
2	刘博	陕西师范大学计算机科学学院	16	48	4.0	6.0