学位论文 > 优秀研究生学位论文题录展示

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

作　者: 胡军
导　师: 李宣东；郑国梁
学　校: 南京大学
专　业: 计算机软件与理论
关键词: 构件化系统设计嵌入式软件设计实时软件系统资源分析能耗分析基于场景的一致性分析模型检验算法接口自动机统一建模语言UML
分类号: TP311.52
类　型: 博士论文
年　份: 2005年
下　载: 743次
引　用: 10次
阅　读: 论文下载

内容摘要

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

全文目录

摘要  3-5
Abstract  5-12
第一章绪论  12-18
  1.1 论文研究的背景及动因  12-13
  1.2 相关研究工作  13-16
  1.3 论文的主要工作  16-17
  1.4 论文的组织  17-18
第二章背景知识  18-27
  2.1 面向对象建模  18-20
  2.2 基于构件的软件工程  20-24
    2.2.1 构件化软件系统  21-23
    2.2.2 接口与构件化设计  23-24
  2.3 形式化方法  24-26
  2.4 本章小结  26-27
第三章接口自动机  27-34
  3.1 接口自动机的非形式描述  27-28
  3.2 接口自动机的形式定义  28-29
  3.3 接口自动机组合  29-30
  3.4 兼容性检查  30-32
  3.5 本章小结  32-34
第四章基于场景规约的一致性验证  34-57
  4.1 一致性验证的相关问题  34-35
  4.2 UML 顺序图的形式化描述  35-38
  4.3 接口自动机网络模型与可达图  38-41
    4.3.1 接口自动机网络  38-40
    4.3.2 兼容状态空间的可达图  40-41
  4.4 存在一致性验证  41-43
    4.4.1 投影路径  41-42
    4.4.2 检验存在一致性  42-43
  4.5 强制一致性验证  43-51
    4.5.1 前向强制一致性验证  43-46
    4.5.2 逆向强制一致性验证  46-49
    4.5.3 双向强制一致性验证  49-51
  4.6 本章小结  51-57
第五章带实时约束场景的一致性验证  57-73
  5.1 带时间约束的顺序图模型  57-59
  5.2 实时接口自动机与构件化实时设计  59-62
    5.2.1 实时接口自动机  59-60
    5.2.2 实时接口自动机网络  60-62
  5.3 带时间约束场景的一致性验证  62-67
    5.3.1 整型状态空间和可达图  63-64
    5.3.2 计算兼容的整型状态空间  64-66
    5.3.3 一致性验证  66-67
  5.4 本章小结  67-73
第六章资源接口与系统资源约束验证  73-87
  6.1 资源使用相关的问题  73-75
  6.2 资源接口自动机（RIA）及自动机网络  75-79
    6.2.1 RIA的非形式描述  75-76
    6.2.2 RIA的形式化定义  76-77
    6.2.3 资源接口自动机网络RIA-Networks  77-79
  6.3 检验系统是否满足给定资源约束  79-81
  6.4 检验给定功能的资源使用合法性  81-85
  6.5 本章小结  85-87
第七章能耗接口与系统能耗分析  87-103
  7.1 能耗性质相关问题  87-89
  7.2 能耗接口自动机（EIA）及其自动机网络  89-92
  7.3 EIA-Networks的整型状态空间与可达图  92-93
  7.4 系统能耗性质分析与验证  93-99
    7.4.1 最少能耗问题  95-97
    7.4.2 最大能耗验证问题  97-99
  7.5 本章小结  99-103
第八章模型检验工具MoCeed的设计  103-107
  8.1 相关验证工具分析  103-104
  8.2 工具的设计原则  104
  8.3 系统的结构和功能  104-106
  8.4 本章小结  106-107
第九章结束语  107-110
  9.1 本文的主要工作  107-108
  9.2 进一步的工作  108-110
参考文献  110-120
攻读博士学位期间参加科研项目及发表论文情况  120-122
致谢  122

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

内容摘要

全文目录

相似论文