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

Java并发程序的模型提取与模型检测技术研究

作　者: 周志远
导　师: 张大方
学　校: 湖南大学
专　业: 软件工程
关键词: Java并发程序模型检测多线程程序分析软件测试
分类号: TP312.2
类　型: 硕士论文
年　份: 2009年
下　载: 164次
引　用: 2次
阅　读: 论文下载

内容摘要

随着多核心处理器系统的发展,分布式并发系统已成为当前主流的软件体系结构。分布式软件的特性导致错误不可重现,使软件排错工作非常困难。Java是在语言级别支持并发的高级语言,其提供的语言特性和大量的类库很好地支持了并发程序的编写。但这些类库都有各自的特点,如果使用不当会造成一些难以发现,却危害严重的问题。同时,Java内存模型JMM(Java Memory Model)允许编译器在优化过程中改变程序的执行顺序,这会让多线程Java程序产生许多意想不到的错误。Java规范中程序的正确性仅仅依赖于程序员编写正确的,不会冲突的代码,很难满足高可靠性软件的要求。针对上述问题,本文提出了一套对Java多线程并发程序错误进行检测的方法。第一部分工作提出了一种自动化模型检测的技术,并制作了工具JTS(Java To SPIN),实现了对Java并发程序的模型检测与验证。JTS对Java程序进行分析,产生抽象语法树,建立程序的抽象模型。分析中特别针对Java虚拟机的并发机制和类库实现进行了建模,并利用模型检测工具SPIN进行了模型检测。在实验中JTS成功地对多个Java程序进行了模型提取和模型检测,给出了错误路径。JTS建立的模型准确地再现了Java程序的执行过程,发现了其中隐藏的并发程序错误。这种检测方法为发现和修正这类不可重现,难以测试的并发错误提供了一种新的方法和思路,是传统测试方法在并行程序领域的的一种尝试与补充。第二部分工作提出了另一种新的方法,针对JMM所允许的程序顺序变化,结合程序中的依赖关系、volatile变量和串行化代码等建立模型,进行模型检测。根据这种检测方法,给出了程序的乱序模型和模型检测结果。在模拟执行和检测结果序列中,可以清楚地看到Java多线程并发程序的乱序执行情况。该方法检测现有JMM规范下所有允许的代码顺序变化,可以发现原有技术无法检测的错误,并给出错误路径,推进了高可靠性Java程序的验证工作。

全文目录

摘要  5-6
Abstract  6-13
第1章绪论  13-24
  1.1 研究背景  13-19
    1.1.1 Java 语言  13-15
    1.1.2 模型检测  15-19
  1.2 相关工作介绍  19-21
  1.3 本课题的研究内容  21-22
  1.4 本文组织结构  22-24
第2章 Java 并发程序分析  24-38
  2.1 Java 的并发机制介绍  24-35
    2.1.1 Java 并发程序锁的问题  25-28
    2.1.2 Java 并发程序的通信问题  28-32
    2.1.3 Java 并发程序的同步问题  32-35
  2.2 JAVACC 简介  35-36
  2.3 JTB 简介  36-37
    2.3.1 产生的文件  36
    2.3.2 自动产生的类  36-37
  2.4 小结  37-38
第3章模型检测理论及工具  38-50
  3.1 模型检测简介  38-40
  3.2 模型检测工具  40-45
    3.2.1 模型检测工具SPIN  40
    3.2.2 SPIN 工作原理及相关定义  40-42
    3.2.3 SPIN 的基本结构  42-43
    3.2.4 SPIN 搜索算法  43-44
    3.2.5 偏序规约  44-45
  3.3 线性时序逻辑LTL  45-46
  3.4 Java 并发程序模型检测  46-49
  3.5 小结  49-50
第4章 Java 并发程序的模型检测  50-64
  4.1 Java 程序分析  50-51
  4.2 建立promela 模型  51-54
    4.2.1 类  52
    4.2.2 方法  52-53
    4.2.3 属性  53
    4.2.4 方法内部语句  53-54
  4.3 Java 并发程序的特殊控制结构  54-59
    4.3.1 锁模型  54-55
    4.3.2 通信控制模型  55-58
    4.3.3 同步控制模型  58-59
  4.4 检测结果  59-60
  4.5 模拟路径分析  60-62
  4.6 实验  62-63
  4.7 小结  63-64
第5章基于Java 内存模型的并发程序模型检测  64-74
  5.1 模型定义与算法  64-66
  5.2 模型建立与检测  66-72
    5.2.1 简单乱序模型  66
    5.2.2 包含Volatile 变量的乱序模型  66-69
    5.2.3 包含依赖关系的乱序模型  69-72
  5.3 小结  72-74
结论  74-76
参考文献  76-80
致谢  80-81
附录 A 攻读学位期间所发表的论文  81-82
附录 B 攻读学位期间所参与的科研活动  82

相似论文

AVS视频解码器在PC平台上的优化及场解码的改善,TN919.81
基于智能学习的多传感器目标识别与跟踪系统研究,TP391.41
基于比对技术的非法网站探测系统的实现与研究,TP393.08
面向对象分层测试的方法研究,TP311.53
基于形式化UML测试序列生成方法研究,TP311.53
基于程序切片的电子海图系统软件测试技术研究,TP311.53
用户权限管理系统可靠性测试的研究与应用,TP311.53
高职院校教学案例库的创建探究,TP311.53-4
基于BMC的Web服务失配检测方法研究,TP311.52
基于中国电信闪铃系统与平台项目的软件测试,TP311.53
民航空管DVOR/DME导航台信号覆盖与飞行程序综合分析及应用研究,V351.37
基于四方的安全电子商务支付协议研究,TP393.08
表面形貌区域法分析评定算法及软件系统研究,TP311.52
基于C/S架构的车辆远程监控系统的设计与实现,TP277
基于多核的动态剖析加速方法研究,TP332
基于Process Engine的Web Services自动化测试研究,TP311.52
自动化测试在分组传输网管接口测试中的应用,TP311.52
基于多线程图像处理机测试系统的研究,TP391.41
一个自动化软件测试系统的设计与实现,TP311.53
基于QTP的SAFFRON自动化测试框架的研究,TP311.52
云备份中的双指纹校验与多线程传输技术研究,TP309.3