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

基于AOP的软件运行时验证关键技术研究

作　者: 张献
导　师: 齐治昌
学　校: 国防科学技术大学
专　业: 计算机科学与技术
关键词: 运行时验证面向方面编程运行时监控器冲突检查预测语义
分类号: TP311.53
类　型: 博士论文
年　份: 2012年
下　载: 49次
引　用: 0次
阅　读: 论文下载

内容摘要

随着信息社会的发展，计算机软件已渗透到日常生活的各个方面，提高计算机软件的可靠性和安全性，以保证其按照人们期望运行的要求变得十分迫切。现有的软件质量保障技术主要包括软件测试、程序分析、模型检测等，但这些技术无法保证最终部署在实际系统上的程序运行时是无错误的。运行时验证（RuntimeVerification）是一种新兴的轻量级验证技术，它把形式化验证技术和系统的实际运行结合起来，监控系统的实际运行，以保证系统的运行与系统关键性质相一致。在运行时验证中，监控器持续监控程序的运行，以判断程序的当前运行轨迹是否满足或违背监控性质。基于面向方面编程技术（Aspect-Oriented Programming，AOP）的软件运行时验证把针对软件的运行时验证当做一个横切关注点来对待，提高了被监控软件系统的模块化程度。由于AOP技术能够把软件运行时验证关注点模块化，同时AOP语言中接入点模型很直观的对应于软件运行时验证中监控事件，基于AOP的软件运行时验证技术在研究界和工业界得到了广泛应用，当前主流的运行时验证框架，如Tracematches，JavaMOP都是基于AOP语言的。随着被监控软件规模增大、并处于不断演化之中，同时运行时验证技术的应用范围在扩展，用户对运行时验证技术检测出问题的时效性也在增强，由于基于AOP的监控器以一种obliviousness方式注入到被监控程序中去，还往往可以对被监控程序进行任意调整，这些都给用户清晰、正确地使用基于AOP的运行时验证技术带来挑战。本文以帮助用户正确、高效使用基于AOP的软件运行时验证技术为目标，提出了一系列语言、方法和技术，帮助用户正确地指定其要监控的性质以及检查针对某一具体程序生成的监控器是否准确反应了用户的监控期望。本文的主要研究贡献包括：1.针对当前基于AOP运行时验证框架提供的事件序列语言不加区分的使用AspectJ中切面语法和不能根据事件间数据流关系选择事件序列的问题，提出了一种运用于软件运行时验证的事件序列选择语言。该事件序列选择语言通过一个受限的切面语法选择单个事件，并有着清晰的层次结构：低层操作符完全通过事件发生的局部环境选择单个事件；高层的操作符利用事件间的控制流和数据流关系选择事件序列。同时，该事件序列语言支持数据流声明，与目前主流的运行时验证框架提供的事件序列选择语言相比，该语言能够表达更细粒度的事件序列。2.针对现行运行时验证中监控事件逐个到达的假设和用户期望更早发现被监控程序的运行是否违背监控性质间的矛盾，提出了面向于运行时验证领域的预测语义。当前的软件运行时验证技术大多都基于监控事件逐个依次到达的假设，这使得监控器只能在故障发生时才能对程序进行调整。如果结合对被监控程序进行静态分析，尽可能多地找出被监控程序运行过程中会产生的监控事件串（序列），这样可以使监控器更早地发现被监控程序的当前运行能否满足或违背监控性质，从而可以对故障进行预测，使用户能够更灵活地进行调整。我们对这种方法进行了形式化的定义，并提供了工具支持。我们使用该工具在几个大型开源项目上进行实验，结果表明带预测语义的运行时验证具有一定的实用性。3.针对基于AOP的运行时验证框架中由于事件选择语言的复杂性引起的性质层面监控器和实现层面监控器间的不一致性以及同一被监控程序上部署的多个监控器相互干扰的问题，提出了基于AOP的监控器内部和监控器之间存在的冲突及相应的检测算法。在基于AOP的软件运行时验证中，由于选择监控事件切面的复杂性，用户在定义监控器时可能会出现在性质层面明确的监控器在实现层面不明确，使得最终生成的监控器没有正确反映用户的监控需求。同时在被监控程序中存在多个监控器注入的情况下，各个监控器间可能互相影响，使得监控器无法依据监控性质正确检测被监控程序的最终运行。针对这些问题，本文第五章对此定义了AOP监控器内部和监控器之间的冲突并提出了相应的自动检测算法，这些定义和检测方法能够帮助用户及时发现监控器中存在的问题，更清楚地掌握其定义的监控器和监控器在被监控程序上的使用。4.针对往被监控程序中注入监控器有可能破坏被监控程序原有重要性质的问题，根据监控器对被监控程序原有性质的影响提出了关于监控器的一个分类框架及自动检测方法。由于当前基于AOP的运行时验证框架允许用户在被监控程序的运行满足或违背监控性质的情况下对被监控程序进行任意调整，这有可能会破坏被监控程序的原来保持的某些重要性质。对此，本文第六章根据监控器对被监控程序原有性质的影响提出了一个基于AOP运行时监控器的分类框架。同时，还根据各种不同类型监控器所具备的一些典型代码特征给出了一个监控器类别检测算法。该分类框架和类别检测算法有助于用户选择正确的监控器和掌控对监控器的使用。

全文目录

摘要  9-11
ABSTRACT  11-13
第一章绪论  13-31
  1.1 软件运行时验证的相关定义  14-19
    1.1.1 软件运行时验证定义  14-15
    1.1.2 判断性质的监控器定义  15
    1.1.3 可修改被监控程序的监控器定义  15-18
    1.1.4 软件运行时验证的应用  18-19
  1.2 软件运行时验证的研究现状  19-27
    1.2.1 运行时验证的性质描述语言  19-22
    1.2.2 LTL公式的有穷语义  22-24
    1.2.3 监控器构造  24-25
    1.2.4 运行时验证性能优化技术  25-27
  1.3 本文的研究内容和贡献  27-29
  1.4 论文结构  29-31
第二章技术和理论基础  31-39
  2.1 面向方面编程  31-34
    2.1.1 模块化横切关注点  31-32
    2.1.2 AOP的接入点模型  32-33
    2.1.3 AspectJ语言介绍  33-34
  2.2 基于AOP的软件运行时验证  34-36
  2.3 可监控和不可监控性质  36-38
  2.4 本章小结  38-39
第三章软件运行时验证的事件选择语言  39-53
  3.1 动机：防范Web程序中的SQL注入攻击  40-42
    3.1.1 SQL注入攻击  40-41
    3.1.2 如何防范SQL注入攻击  41
    3.1.3 用运行时验证防范SQL注入攻击  41-42
  3.2 选择单个事件的切面语法  42-43
    3.2.1 AspectJ切面的语法  42-43
    3.2.2 选择单个事件的切面语法  43
  3.3 软件运行时验证的事件选择语言  43-45
  3.4 软件运行时验证的事件选择语言的表达能力  45-48
  3.5 工具实现和案例研究  48-50
    3.5.1 工具实现  48-49
    3.5.2 案例研究  49-50
  3.6 相关工作  50-51
  3.7 本章小结  51-53
第四章带预测语义的软件运行时验证  53-71
  4.1 背景知识介绍  53-54
    4.1.1 Büchi自动机  53-54
    4.1.2 三值语义的软件运行时验证  54
  4.2 带预测语义的软件运行时验证  54-56
  4.3 基于预测语义的监控器构造和检测  56-60
    4.3.1 基于预测语义的监控器构造  57-59
    4.3.2 带预测语义的监控器检测过程  59-60
    4.3.3 监控器示例  60
  4.4 支持预测语义的工具实现  60-66
    4.4.1 工具支持的预测语义  61-62
    4.4.2 把LTL公式转化为监控器  62-63
    4.4.3 插装被监控程序  63-66
  4.5 案例研究与实验  66-68
    4.5.1 案例研究  66-67
    4.5.2 实验和结果分析  67-68
  4.6 相关工作  68-70
  4.7 本章小结  70-71
第五章基于AOP的运行时验证中的冲突检测  71-87
  5.1 基于AOP的面向运行时监控的事件选择表达式  72-74
  5.2 单个监控器内的冲突检测  74-79
    5.2.1 单个监控器内冲突的定义  74-76
    5.2.2 单个监控器内冲突的检测算法  76-79
  5.3 多个监控器间的冲突检测  79-82
    5.3.1 多个监控器间冲突的定义  79-80
    5.3.2 多个监控器间冲突的检测算法  80-82
  5.4 实现与案例研究  82-84
  5.5 相关工作  84-85
  5.6 本章小结  85-87
第六章基于AOP的运行时监控器的分类和检测方法  87-109
  6.1 运行时验证框架中监控器的定义  88-91
    6.1.1 JavaMOP中监控器示例  89-91
  6.2 基于AOP运行时监控器的分类  91-97
    6.2.1 被监控程序的语义  91-94
    6.2.2 基于AOP运行时监控器的分类  94-96
    6.2.3 监控器类别与被监控程序保持性质间的关系  96-97
  6.3 基于AOP监控器类别的自动检测方法  97-101
  6.4 工具实现和实验结果分析  101-104
    6.4.1 工具实现  101-102
    6.4.2 实验及结果分析  102-104
  6.5 相关工作  104-106
  6.6 本章小结  106-109
第七章结束语  109-113
  7.1 本文的主要工作  109-110
  7.2 进一步的工作展望  110-113
致谢  113-115
参考文献  115-127
作者在学期间取得的学术成果  127-128

基于AOP的软件运行时验证关键技术研究

内容摘要

全文目录

相似论文