嵌入式基于模型驱动验证及软件生产线的研究与实现

论文摘要

随着处理器的计算能力的迅速提高、嵌入式技术的迅猛发展和嵌入式系统应用领域的不断拓宽,使得嵌入式软件的规模以及复杂性的不断增长,从而导致了开发时间和费用也在不断的增长,如何快速有效的开发嵌入式软件成为目前亟待解决的问题。为了解决上面的问题,全球最大的软件工业标准化组织OMG (Object Management Group)提出了模型驱动框架MDA (Model Driven Architecture)开发方法。MDA方法将软件开发过程分成两个主要阶段：模型级和代码级。模型主要关注系统的设计正确性,从而达到以较小代价修改软件错误的目的。面向嵌入式软件的开发工具目前正在从基于代码的传统开发环境向基于模型的开发环境发展。而一个基于模型的嵌入式生产线开发环境,应该是集成模型开发工具和其他相关工具,包含了建模、模型仿真验证、代码生成、测试等嵌入式软件开发的全过程。这符合嵌入式软件开发工具发展趋势,也具备相应的理论、技术和产品基础。模型驱动验证是基于模型的嵌入式软件生产线的一个重要部分,这个关键部分会影响到系统的质量和后期的工作,如果在前期能够及时发现出存在的问题,可以节省大量的人力物力。当今主流的嵌入式实时系统中,实时性是一个关键的性能指标,对于这类系统就是要求它们在合法的时间内完成相应的行为,不会发生超时现象,这就要求验证任务间的可调度性来判断系统实时性是否符合要求。由Clark和Emerson提出形式化的模型验证的方法以开始应用在任务的可调度分析上,该方法的基本原理是为要检测的系统建立形式化模型,阐明所要验证的性质,然后使用算法去检查该模型是否满足所述性质。本文的研究是基于模型的软件嵌入式生产线开发环境,在这条主线上把重点放在研究和解决模型方面的形式化验证问题,对嵌入式模型实时性中的可调度问题进行研究。论文先介绍了基于模型的嵌入式软件生产线的背景与意义,并分析了国内外的发展情况,接着说明课题的来源和本文研究的内容；在此基础上提出基于模型的嵌入式生成线的总体需求分析；接着重点介绍模型验证调度检测工具SCT (Scheduling Check Tool)的设计,包括SCT所分析的系统的相关定义和规定以及任务的两个行为自动机模型的设计实现,在这些前提下对SCT工具进行总体设计,并对每部分进行实现,其中重点放在调度仿真算法进行设计与实现；接着在LambdaPRO的基础上集成相关工具,实现基于模型的嵌入式软件生成线的整个开发过程,并通过一个实例应用来说明验证这个开发流程。论文最后对本文的工作进行总结,并对后继研究和发展进行了展望。

论文目录

• 摘要
• ABSTRACT
• 第1章 绪论
• 1.1 背景及意义
• 1.2 国内外情况
• 1.2.1 模型驱动
• 1.2.2 模型驱动验证
• 1.3 课题来源
• 1.4 本文研究内容及论文结构
• 1.4.1 本文研究内容
• 1.4.2 论文结构
• 第2章 基于模型的嵌入式软件生产线需求分析
• 2.1 生产线的生产流程
• 2.2 开发过程需求
• 2.2.1 向导需求
• 2.2.2 集成模型开发工具的需求
• 2.2.3 模型驱动验证需求
• 2.2.4 代码转换和合成需求
• 2.3 本章小结
• 第3章 调度分析系统模型的设计
• 3.1 调度系统模型的设计
• 3.2 任务模型的设计
• 3.3 外部事件自动机
• 3.3.1 时间自动机理论
• 3.3.2 外部事件自动机的设计
• 3.3.3 任务被激活的实例数
• 3.3.4 外部事件自动机的数据结构
• 3.4 内部状态自动机
• 3.4.1 内部状态自动机的定义
• 3.4.2 内部状态自动机模型
• 3.4.3 内部状态自动机的数据结构
• 3.5 本章小结
• 第4章 调度检测工具SCT的设计与实现
• 4.1 SCT体系结构设计
• 4.2 系统信息收集设计
• 4.2.1 编辑面板结构
• 4.2.2 信息的输入与存储
• 4.2.3 模型行为自动机实例化
• 4.3 DBM的设计与实现
• 4.3.1 DBM存储结构设计
• 4.3.2 DBM关键操作
• 4.4 调度仿真树的设计
• 4.4.1 可达性判断
• 4.4.2 调度仿真树的定义
• 4.4.3 调度仿真树的数据结构
• 4.4.4 调度仿真树的构造和处理流程
• 4.5 调度分析过程的设计
• 4.5.1 调度分析算法总流程
• 4.5.2 时间流逝处理
• 4.5.3 求后继状态的算法设计
• 4.5.4 消息队列的处理
• 4.4.5 抢占处理
• 4.6 仿真模拟分析设计
• 4.6.1 仿真算法总流程
• 4.6.2 时间流逝值模拟
• 4.7 本章小结
• 第5章 基于模型的嵌入式软件生产线的设计与实现
• 5.1 生产线的系统设计
• 5.2 工程项目向导设计
• 5.2.1 MDE项目向导
• 5.2.2 Mdl文件向导
• 5.3 OSATE与LambdaPRO的集成
• 5.4 Simulink的集成
• 5.5 AADL模型验证
• 5.6 Simulink模型测试
• 5.6.1 静态测试的实现
• 5.6.2 覆盖测试的实现
• 5.6.3 过滤器的实现
• 5.7 代码转换及代码合成
• 5.7.1 模型的代码转换
• 5.7.2 代码合成实现
• 5.8 本章小结
• 第6章 软件生产线开发环境验证
• 第7章 总结与展望
• 7.1 总结
• 7.2 展望
• 致谢
• 参考文献
• 攻读硕士学位期间发表的论文