AADL模型可调度性分析工具设计与实现

摘要

随着计算机应用领域的不断扩张，计算机软件的开发规模逐渐扩大，软件复杂度不断增加，开发周期和开发成本也不断增长。为了解决这些问题，对象管理组织(OMG)提出了模型驱动结构方法(Model Driven Architecture)。MDA的核心思想是以模型为中心，将模型和实现分离，使软件开发过程简化为建立业务逻辑模型后由机器自动生成特定计算平台的代码。在MDA中，建模语言不仅仅是设计语言，也是编程语言。
　　 针对嵌入式领域中的软件开发复杂度问题，业界提出一种基于MDA方法的体系结构建模语言--体系结构分析设计语言(Architecture Analysis and Design Language，AADL)。AADL是用于设计和分析安全关键的嵌入式实时系统的软件和硬件体系结构的建模语言，围绕AADL的开发平台及模型验证工具的开发逐渐成为热点。
　　 MDA的核心是模型，而模型设计是否满足需求则需要其它工具来进行测试验证。本论文基于带时钟约束的混合自动机理论，设计了一种对AADL模型的可调度性进行形式化验证的工具。
　　 论文首先介绍了目前关于AADL模型的可调度性验证的研究情况及已开发的工具，并分析了各种工具的缺陷。然后简要介绍了AADL的概念及时间自动机理论。在此基础上，对使用UPPAAL工具对AADL模型进行可调度性验证进行了实践。实践表明UPPAAL工具无法进行可抢占调度策略下的AADL模型的可调度性验证。因此，论文在带时钟约束的混合自动机理论基础上进行了AADL可调度性验证工具UCaS的设计开发。论文按照软件工程方法分模块详细说明UCaS的设计、涉及的技术及关键代码，并对UCaS工具的性能进行了测试。论文最后总结了UCaS工具的优点及局限性，对AADL模型验证工具的后继研究和发展进行了展望。

目录

文摘

英文文摘

声明

第1章绪论

1.1选题背景及意义

1.2国内外研究概况及发展趋势

1.3课题研究方法

1.4本文的内容和组织

第2章AADL与时间自动机理论

2.1 AADL概述

2.1.1端口

2.1.2线程组件

2.1.3进程组件

2.1.4处理器组件

2.1.5关联

2.1.6 AADL简单模型

2.2时间自动机及可达性判断

2.2.1时间自动机理论概述

2.2.2可达性判断原理

第3章基于UPPAAL的AADL模型验证

3.1 UPPAAL概述

3.2 OSATE工具概述

3.3设计UPPAAL中的调度模型

3.2.1周期及零星线程模板

3.2.2非周期线程模板

3.2.3调度器模板

3.2.4周期线程事件产生器模板

3.2.5非周期及零星线程事件产生器模板

3.4可调度性验证及局限性

第4章UCaS工具的设计与实现

4.1总体设计

4.1.1系统结构设计

4.1.2用户界面设计

4.1.3混合自动机理论

4.2数据采集设计与实现

4.2.1设计思路

4.2.2类层次结构设计

4.2.3 AAXL实例文件的访问

4.3事件产生器设计与实现

4.3.1设计思路

4.3.2 XML文件生成及解析

4.3.3图形编辑器的设计与实现

4.4调度分析设计与实现

4.4.1设计思路

4.4.2差值有界矩阵及基本操作

4.4.3线程自动机的设计

4.4.4类层次结构设计

4.4.5可调度性分析算法设计

4.5调度仿真设计与实现

4.5.1设计思路

4.5.2带滚动条和横向标尺的窗口

4.5.3调度仿真的连续执行

4.5.4定位当前绘制点及面板大小调整

4.5.5双缓存技术解决绘图闪烁

4.5.6避免内存泄露

4.5.7显示鼠标位置的刻度值

4.5.8甘特图的绘制

4.6插件的设计及实现

第5章UCaS工具测试

5.1 UCaS工具运行测试

5.1.1测试环境

5.1.2测试用例设计

5.1.3测试过程及结果说明

5.2 UCaS工具性能测试

5.2.1测试环境

5.2.2测试用例设计

5.2.3测试结果及说明

结 论

致 谢

参考文献

攻读硕士学位期间发表的论文