[1]刘博 李蜀瑜.基于NuSMV的AADL行为模型验证的探究[J].计算机技术与发展,2012,(02):110-113.
LIU Bo,LI Shu-yu.AADL Behavior Based on NuSMV Model Validation of Inquiry[J].,2012,(02):110-113.
点击复制
基于NuSMV的AADL行为模型验证的探究(
)
《计算机技术与发展》[ISSN:1006-6977/CN:61-1281/TN]
- 卷:
-
- 期数:
-
2012年02期
- 页码:
-
110-113
- 栏目:
-
智能、算法、系统工程
- 出版日期:
-
1900-01-01
文章信息/Info
- Title:
-
AADL Behavior Based on NuSMV Model Validation of Inquiry
- 文章编号:
-
1673-629X（2012）02-0110-04
- 作者:
-
刘博 李蜀瑜
-
陕西师范大学计算机科学学院
- Author(s):
-
LIU Bo; LI Shu-yu
-
Dept.of Computer Science,Shaanxi Normal University
-
- 关键词:
-
嵌入式构件分析与设计语言; AADL集成开发环境; 行为模型; NuSMV验证方法
- Keywords:
-
AADL; OSATE; behavior model; NuSMV validation methods
- 分类号:
-
TP31
- 文献标志码:
-
A
- 摘要:
-
鉴于模型在软件系统开发中日趋重要的地位和AADL模型在嵌入式软件建模中的良好应用前景,为了在嵌入式软件系统开发前期保证AADL模型的质量,提出了一种基于模型测试的AADL架构和NuSMV模型的验证方法。文中首先对当前的AADL发展情况作简单介绍,然后对NuSMV验证模型的结构作大致分析,在随后的文章中对NuSMV的验证过程作详细的介绍。与此同时,使用具体的汽车巡航控制系统作为实例进行具体分析。文中通过测试用例执行输出进行验证来判断该方法的正确性
- Abstract:
-
As models take important part in software development and AADL can describe embedded software effectively,a method for AADL model and NuSMV model testing is put forward to insure the quality of the models in early step of software developing.Proposed a test based on the AADL architecture model and NuSMV model validation methods.The development of the current AADL is introduced briefly,then the structure of the NuSMV model validation is analysed,in the subsequent article in the verification process of the NuSMV is described in detail.At the same time,the use of specific automobile cruise control system as the example is analysed.At last,verify the correctness of the method through an example
备注/Memo
- 备注/Memo:
-
中央高校基本科研业务费专项资金（GK201002011）; 教育部科学教育重点项目（107106）刘博（1988-），男（回族），河南郑州人，硕士研究生，主要研究领域嵌入式系统；李蜀瑜，副教授，博士，主要研究领域为嵌入式系统、Web服务
更新日期/Last Update:
1900-01-01