基于UPPAAL的嵌入式系统AADL模型实时性验证

发布时间：2017-05-11 13:10

  本文关键词：基于UPPAAL的嵌入式系统AADL模型实时性验证，由笔耕文化传播整理发布。

【摘要】：随着嵌入式系统的规模、复杂程度和可靠性需求的不断提升，模型驱动的体系结构开发方法已经成为复杂嵌入式系统开发的主流。体系结构分析与设计语言AADL（ArchitectureAnalysisand Design Language, AADL）是嵌入式实时系统领域模型驱动方法的新标准，在支持系统软、硬件结构建模的同时可对可靠性、实时性等非功能属性的描述，可在模型驱动开发过程早期的模型建立阶段，通过形式化的模型检验方法对系统模型的关键属性进行验证，及早发现设计过程中潜在的错误，对保障系统实时性和提高开发效率都具有重要的意义。 为了对AADL模型的可调度性和数据流时延特性进行验证，本文采用时间自动机形式化模型检验方法建立了AADL模型中调度模型和数据流的时间自动机，实现了从AADL模型到时间自动机模型的转换和验证工作。在调度模型时间自动机的建立中，，设计了周期、非周期的线程模板以及抢占和非可抢占的调度器模板，通过模型转换法则将AADL调度模型转换到时间自动机模型。在数据流的模型转换中，分别设计了单一数据流和混合数据流到时间自动机的转换方法，混合数据流转换得到的时间自动机可与调度模型时间自动机构成时间自动机网络，实现了数据流与调度模型的综合分析与验证。 利用Eclipse的插件开发技术，设计了自动化模型转换插件并将其集成到AADL的建模工具OSATE中，实现了建模、转换、验证与分析过程的集成开发环境。最后利用时间自动机建模与验证工具UPPAAL对转换得到的时间自动机进行模拟和验证，等价地验证原AADL模型的设计是否满足实时性要求。测试数据表明，所建立模型转换方法能有效地将AADL模型转换到时间自动机模型，在UPPAAL中能够正确地分析原模型的可调度性和数据流时延特性。
【关键词】：AADL 时间自动机 可调度性 数据流时延 模型转换 UPPAAL
【学位授予单位】：南京航空航天大学
【学位级别】：硕士
【学位授予年份】：2014
【分类号】：TP368.1
【目录】：

• 摘要4-5
• ABSTRACT5-6
• 目录6-9
• 图表清单9-11
• 注释表11-12
• 第一章 绪论12-18
• 1.1 研究的背景与意义12-13
• 1.2 国内外研究现状及存在的问题13-15
• 1.2.1 国内外研究现状分析13-14
• 1.2.2 目前研究存在的问题14-15
• 1.3 论文研究内容及章节安排15-18
• 第二章 体系结构分析设计语言与时间自动机18-29
• 2.1 AADL 概述18-22
• 2.1.1 组件19-20
• 2.1.2 端口和连接20
• 2.1.3 语法20-21
• 2.1.4 建模实例21-22
• 2.2 时间自动机22-25
• 2.2.1 时间自动机简介22
• 2.2.2 时间自动机理论22-24
• 2.2.3 基于时间自动机的验证24-25
• 2.3 UPPAAL25-28
• 2.3.1 UPPAAL 的扩展元素25-27
• 2.3.2 UPPAAL 中的性质验证语句27-28
• 2.4 本章小结28-29
• 第三章 AADL 调度模型的转换与验证29-52
• 3.1 引言29-30
• 3.2 AADL 调度模型到时间自动机模型的语义映射30-33
• 3.2.1 AADL 调度模型语义30-31
• 3.2.2 线程执行状态机31-32
• 3.2.3 模型转换语义映射32-33
• 3.3 调度模型时间自动机设计33-46
• 3.3.1 符号说明34-35
• 3.3.2 非可抢占调度策略时间自动机设计35-40
• 3.3.3 可抢占调度策略时间自动机设计40-46
• 3.4 可调度性验证语句46-47
• 3.5 时间自动机模型正确性检验47-48
• 3.6 AADL 调度模型到时间自动机模型转换方法48-51
• 3.6.1 调度模型转换流程48-49
• 3.6.2 线程优先级计算策略49-50
• 3.6.3 线程组件到线程时间自动机模板的转换示例50-51
• 3.7 本章小结51-52
• 第四章 AADL 数据流的转换与验证52-62
• 4.1 引言52-53
• 4.2 AADL 数据流53-55
• 4.2.1 数据流简介53-54
• 4.2.2 数据流的形式化描述54-55
• 4.3 数据流到时间自动机的转换55-60
• 4.3.1 单一数据流转换方法55-57
• 4.3.2 混合数据流转换方法57-60
• 4.4 数据流性质验证语句60
• 4.5 数据流转换方法检验60-61
• 4.6 本章小结61-62
• 第五章 模型转换插件的设计与系统测试62-74
• 5.1 引言62
• 5.2 模型转换插件功能设计62-64
• 5.3 AADL 模型解析模块64-66
• 5.3.1 AADL 模型文件分析64-65
• 5.3.2 AADL 对象模型构建65-66
• 5.4 模型转换模块66
• 5.5 时间自动机模型生成模块66-68
• 5.5.1 UPPAAL 模型文件分析67-68
• 5.5.2 时间自动机对象模型构建及模型文件生成68
• 5.6 插件开发技术68-69
• 5.7 模型转换及验证测试69-73
• 5.7.1 测试环境70
• 5.7.2 组合测试用例70
• 5.7.3 测试方法70-71
• 5.7.4 测试结果实例展示71-72
• 5.7.5 性能分析72-73
• 5.8 本章小结73-74
• 第六章 总结与展望74-75
• 6.1 总结74
• 6.2 展望74-75
• 参考文献75-79
• 致谢79-80
• 攻读硕士学位期间发表的学术论文80

【参考文献】

中国期刊全文数据库 前3条

1 朱雪阳,唐稚松;基于时序逻辑的软件体系结构描述语言XYZ/ADL[J];软件学报;2003年04期

2 王永吉,陈秋萍;单调速率及其扩展算法的可调度性判定[J];软件学报;2004年06期

3 程永江;周清雷;;基于uppaal的飞机着陆控制系统模型验证[J];计算机工程与设计;2009年23期

  本文关键词：基于UPPAAL的嵌入式系统AADL模型实时性验证，由笔耕文化传播整理发布。

本文编号：357313