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

基于运行时验证的AOP程序检测框架研究

作　者: 梁睿
导　师: 吴尽昭
学　校: 兰州大学
专　业: 计算机软件与理论
关键词: 面向切面编程运行时验证模型检测连接点线性时序逻辑注解
分类号: TP311.52
类　型: 硕士论文
年　份: 2009年
下　载: 62次
引　用: 1次
阅　读: 论文下载

内容摘要

面向对象编程(Obiect-Oriented Programming,OOP)是一种实现软件模块化和可重用的编程规范,较好地解决对象和数据的封装问题。但是随着编程实践的日益丰富,OOP也表现出缺陷:在加入横切关注之后的代码容易产生交织、分散问题,使得代码难以理解和维护。面向切面编程(Aspect-OrientedProgramming,AOP)方法应运而生,为上述问题提供了一种有效和可行的方法:AOP支持软件模块化和可重用,能有效地消除代码的交织和分散问题。AOP将程序被描述成对象和切面的集合,通过织入器把切面织入到程序中。由于切面如何描述在很大程度上影响到系统的关键行为(比如性能和同步),与此同时,系统的关键行为使得切面的描述复杂化,Bugs可能存在于程序中而难以发觉。因此AOP程序的验证工作相对复杂。我们需要一种方法来测试或验证AOP程序的正确性。目前对AOP的研究侧重于语言本身的实现和应用,而对程序进行检查和验证的相关研究十分缺乏。针对目前的需求,本文提出一种基于运行时验证的框架来检测AOP程序,使得AOP程序中横切关注点的验证得以实现。在这种框架中,程序的性质由线性时序逻辑公式描述,并在程序执行时使用运行时验证技术来验证。本文给出该框架的整体流程和核心算法,并使用一个详细的案例对研究内容进行分析介绍。

全文目录

摘要  4-5
ABSTRACT  5-7
目录  7-9
第一章绪论  9-14
  1.1 研究背景  9-10
  1.2 相关研究  10-11
  1.3 本文主要工作  11-12
  1.4 本文组织结构  12-14
第二章 AOP语言及其实现机制  14-20
  2.1 AOP产生的背景  14-15
    2.1.1 传统编程方法学面临的问题  14
    2.1.2 AOP的产生  14-15
  2.2 AOP核心概念  15-17
    2.2.1 横切  15
    2.2.2 核心关注点和横切关注点  15
    2.2.3 切面  15-16
    2.2.4 连接点和切点  16
    2.2.5 通知  16-17
    2.2.6 织入  17
  2.3 AOP织入实现机制  17-18
  2.4 ASPECTJ简介  18
  2.5 JAVA5注解  18-20
第三章运行时验证概述及验证方法  20-24
  3.1 运行时验证产生的背景  20-21
  3.2 运行时验证概述  21-22
  3.3 运行时验证的执行流程  22-23
  3.4 运行时验证特点  23-24
第四章运行时验证理论基础  24-35
  4.1 线性时序逻辑  24-27
    4.1.1 线性时序逻辑的语法  24-25
    4.1.2 线性时序逻辑的语义  25-26
    4.1.3 线性时序逻辑的NNF范式  26-27
  4.2 自动机理论  27-35
    4.2.1 在有限字上的自动机  27-29
    4.2.2 在无限字上的自动机  29-32
    4.2.3 线性时序逻辑公式到自动机的转换  32-35
第五章使用运行时验证检测AOP程序  35-47
  5.1 AOP程序验证简介  35-36
  5.2 运行时验证中的核心算法  36-41
  5.3 验证框架  41-44
  5.4 代码举例  44-47
第六章总结与展望  47-49
参考文献  49-52
在学期间的研究成果  52-53
致谢  53

相似论文

基于BMC的Web服务失配检测方法研究,TP311.52
顾问型企业项目管理系统的设计与实现,TP311.52
基于四方的安全电子商务支付协议研究,TP393.08
输电系统可靠性统计评价方法研究及应用,TM732
安全协议自动化分析系统的设计与实现,TP393.08
Web服务事务协调协议WS-TX的形式化分析与验证,TP393.09
基于UPPAAL的电子商务协议安全性分析,TP393.08
软件行为运行时验证研究,TP311.52
LMCCD影像像点自动量测技术研究,TP391.41
基于模型检测方法的可信软件验证技术研究,TP311.52
面向环境演算系统的模型检测算法的研究,TP274
网络安全协议的模型检测分析及验证系统,TP393.08
基于程序语义的静态恶意代码检测系统的研究与实现,TP393.08
可重配置硬件系统调度算法的模拟与分析,TN791
《昭通方言疏证》研究,H17
基于运行时验证的列控系统形式分析,TP273
杜甫文赋注解研究,I207.22
时间感知Web服务交互适配技术研究,TP393.09
基于XYZ/ADL的Web服务组合验证研究,TP393.09
基于Color Petri Nets的HMIPv6协议形式化验证研究,TN929.5
基于SVO逻辑的多方不可否认协议的形式化分析与研究,TP393.08