构件化嵌入式软件设计的分析与验证

论文题目: 构件化嵌入式软件设计的分析与验证

论文类型: 博士论文

论文专业: 计算机软件与理论

作者: 胡军

导师: 李宣东,郑国梁

关键词: 构件化系统设计,嵌入式软件设计,实时软件系统,资源分析,能耗分析,基于场景的一致性分析,模型检验,算法,接口自动机,统一建模语言

文献来源: 南京大学

发表年度: 2005

论文摘要: 近年来随着计算机硬件性能的不断提高,嵌入式系统中软件系统的规模和复杂性不断增加,从而软件对整个系统的影响逐渐占据了统治地位,嵌入式软件已成为近几年来人们研究的热点。嵌入式软件具有极高的可靠性、严格的实时性需求以及资源使用的受限性、满足特定领域等要求,使得如何保证系统设计满足给定的功能规约,以及满足资源、能耗等非功能方面的严格限制成为嵌入式计算领域中的重要研究课题。基于构件的设计方法学已逐渐成为现在软件工程的主流,它通过复用和组合软件模块来构造系统,从而可以提高系统开发效率和可靠性。嵌入式系统通常是由多个计算子系统构成,其软件系统具有较高的构件化特征,构件之间的交互场景是体现系统行为复杂性的一个重要方面。作为一种描述构件接口性质的形式化语言,接口自动机刻画了构件以及外部环境之间交互行为的时序特征,可以用来对构件化嵌入式软件的行为进行有效的建模与分析。本文以接口自动机作为嵌入式软件的基本设计模型,对构件化嵌入式软件设计阶段有关系统行为的功能以及非功能方面性质进行形式化分析与验证,主要工作包含以下几个方面:1.针对基于场景的功能规约与系统动态行为之间的一致性问题,通过对UML顺序图模型和接口自动机网络的分析,分别研究了存在一致性、前向强制一致性、逆向强制一致性以及双向强制一致性等重要性质,并给出了相应的一致性语义分析和验证算法。2.针对系统实时行为一致性分析与验证问题,使用时间布尔不等式对UML顺序图模型进行实时扩展,在接口自动机基本模型中添加时间区间增强其对系统实时行为的描述能力。通过对实时接口自动机网络的状态空间的分析,构造了其可兼容的整型状态等价类空间的可达图,并在此基础上给出了实时行为一致性验证算法。3.研究了在资源严格受限的约束条件下,系统运行过程中对资源使用的兼容性检查问题。通过对接口自动机基本模型进行资源使用约束方面的语义扩展,分析了资源接口组合模型的行为,给出了判断资源使用兼容性的验证算法;并在此基础上对指定的系统功能的资源使用性质进行了分析与验证。4.基于嵌入式系统能耗性质的分析,对实时接口自动机模型进行能耗约束方面的扩展,建立了能耗接口模型,研究了在有限能源供给的系统中软件运行能耗相关性质的检查和计算问题。通过对能耗接口组合模型的状态空间的分析,给出了针对最少耗能计算和最大能耗验证两个典型问题的相关算法。5.设计了一个嵌入式软件系统动态模型的分析和验证原型工具。工具可以对嵌入式软件系统实时和非实时的一致性问题、资源使用兼容性检查问题以及能耗方面的相关性质等进行自动化分析与验证,并给出相应的结果以及反例信息。

论文目录:

摘要

Abstract

第一章 绪论

1.1 论文研究的背景及动因

1.2 相关研究工作

1.3 论文的主要工作

1.4 论文的组织

第二章 背景知识

2.1 面向对象建模

2.2 基于构件的软件工程

2.2.1 构件化软件系统

2.2.2 接口与构件化设计

2.3 形式化方法

2.4 本章小结

第三章 接口自动机

3.1 接口自动机的非形式描述

3.2 接口自动机的形式定义

3.3 接口自动机组合

3.4 兼容性检查

3.5 本章小结

第四章 基于场景规约的一致性验证

4.1 一致性验证的相关问题

4.2 UML 顺序图的形式化描述

4.3 接口自动机网络模型与可达图

4.3.1 接口自动机网络

4.3.2 兼容状态空间的可达图

4.4 存在一致性验证

4.4.1 投影路径

4.4.2 检验存在一致性

4.5 强制一致性验证

4.5.1 前向强制一致性验证

4.5.2 逆向强制一致性验证

4.5.3 双向强制一致性验证

4.6 本章小结

第五章 带实时约束场景的一致性验证

5.1 带时间约束的顺序图模型

5.2 实时接口自动机与构件化实时设计

5.2.1 实时接口自动机

5.2.2 实时接口自动机网络

5.3 带时间约束场景的一致性验证

5.3.1 整型状态空间和可达图

5.3.2 计算兼容的整型状态空间

5.3.3 一致性验证

5.4 本章小结

第六章 资源接口与系统资源约束验证

6.1 资源使用相关的问题

6.2 资源接口自动机（RIA）及自动机网络

6.2.1 RIA的非形式描述

6.2.2 RIA的形式化定义

6.2.3 资源接口自动机网络RIA-Networks

6.3 检验系统是否满足给定资源约束

6.4 检验给定功能的资源使用合法性

6.5 本章小结

第七章 能耗接口与系统能耗分析

7.1 能耗性质相关问题

7.2 能耗接口自动机（EIA）及其自动机网络

7.3 EIA-Networks的整型状态空间与可达图

7.4 系统能耗性质分析与验证

7.4.1 最少能耗问题

7.4.2 最大能耗验证问题

7.5 本章小结

第八章 模型检验工具MoCeed的设计

8.1 相关验证工具分析

8.2 工具的设计原则

8.3 系统的结构和功能

8.4 本章小结

第九章 结束语

9.1 本文的主要工作

9.2 进一步的工作

参考文献

攻读博士学位期间参加科研项目及发表论文情况

致谢

发布时间: 2007-10-25

参考文献

• [1].面向业务构件的可重构信息系统的模型研究[D]. 李绪蓉.南京航空航天大学2002
• [2].CAPP领域构件复用技术研究[D]. 柯文.南京航空航天大学2003
• [3].基于构件的制造执行系统产品线关键技术研究[D]. 任守纲.南京航空航天大学2005
• [4].嵌入式实时软件的构件化开发技术研究[D]. 古幼鹏.电子科技大学2005
• [5].多内核构件化嵌入式操作系统的研究[D]. 谢铖.浙江大学2006
• [6].基于构件的支持群体工作环境中若干问题研究[D]. 马晓龙.中国科学院研究生院（计算技术研究所）2000
• [7].基于信息链的智能信息处理关键技术研究[D]. 张瑞军.武汉理工大学2007
• [8].商业构件评估方法及关键技术研究[D]. 盛津芳.中南大学2007
• [9].基于本体的构件检索研究[D]. 唐彬.复旦大学2007
• [10].复杂流程分布式控制系统构件研究与模型变换[D]. 刘晓燕.昆明理工大学2007

相关论文

• [1].嵌入式系统的硬/软件协同设计研究[D]. 程国达.复旦大学2003
• [2].基于UML的嵌入式系统系统级设计方法研究[D]. 陈燕.复旦大学2005
• [3].基于异构多核体系与组件化软件的嵌入式系统研究[D]. 戴鸿君.浙江大学2007
• [4].可重构嵌入式系统样机平台与操作系统研究[D]. 周学功.复旦大学2007
• [5].可重构嵌入式系统快速原型方法及任务调度算法研究[D]. 梁梁.复旦大学2007
• [6].面向方面技术在大规模嵌入式软件中的应用[D]. 邓阿群.浙江大学2007

标签：构件化系统设计论文;  嵌入式软件设计论文;  实时软件系统论文;  资源分析论文;  能耗分析论文;  基于场景的一致性分析论文;  模型检验论文;  算法论文;  接口自动机论文;  统一建模语言论文;