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

摘要：

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

关键词：嵌入式构件分析与设计语言、AADL集成开发环境、行为模型、NuSMV验证方法

所属期刊栏目：22

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

资助基金：中央高校基本科研业务费专项资金GK201002011;教育部科学教育重点项目107106

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

页数：共4页

页码：110-113