基于jml垃圾收集验证

《基于jml垃圾收集验证》由会员上传分享，免费在线阅读，更多相关内容在学术论文-天天文库。

1、中图分类号：TP391UDC：004学校代码：10004密级：公开lIIIIIIIIIIIIIIIIIIIllIIIUIY2427830北京交通大学硕士学位论文基于JML的垃圾收集验证VerificationofGarbageCollectionwithJML作者姓名：宋玉婷导师姓名：孙文辉学位类别：工学学科专业：计算机科学与技术学号：10120506职称：副教授学位级别：硕士研究方向：软件测试北京交通大学2013年6月致谢“雄关漫道真如铁，而今迈步从头越”。转眼间，这段研究生求学生活即将结束，在即将走出校园

2、之际，回首往昔，奋斗、辛劳、欢笑、泪水也都历历在目。留恋之情，油然而生。北京交通大学学风优良、科研氛围浓厚、宽容博大，教我成才、成人。值此毕业论文完成之际，我谨向所有关心、爱护、帮助我的人们表示最诚挚的感谢与最美好的祝愿。首先，我要感谢我的恩师孙文辉老师为我付出的心血。这篇论文是在恩师的悉心指导下完成的，从一开始确定题目、收集相关材料、到实验分析、一轮轮的修改、到最终定稿，孙文辉老师给了我耐心的指导和无私的帮助。师恩如海，衔草难报。孙文辉老师严谨治学、知识渊博、精益求精、勤奋敬业、质朴高尚，为我树立了终生的学

3、习典范，他的教诲和鞭策将激发我在未来人生的道路上励精图治、开拓创新。除此之外，孙文辉老师在学习上和生活上都给予了我很大的关心和帮助，我自豪有一位这样的老师，他值得我感激和尊敬，在此向孙文辉老师表示衷心的谢意。本论文的完成也离不开其他各位老师、同学和朋友的关心与帮助。在此也要感谢各位老师在论文开题期间给出珍贵意见，同时感谢研究生期间给我传授专业知识的任课老师和生活中常常给予我们帮助的郭神华、平洋老师，还有其他同学对我的支持和帮助。另外也感谢我的父母，没有你们，就不会有今天的我!他们对我莫大的理解和支持使我能够在

4、学校专心完成我的学业，焉得谖草，言树之背，养育之恩，无以回报。中文摘要摘要：垃圾收集已经普遍应用于主流的软件开发领域中，有效地避免了一些安全漏洞的同时提高了资源利用率。然而，垃圾收集自身都比较复杂，其算法设计和实现的可靠性往往难以保证。对于和用户程序并行执行的垃圾收集器，其交互过程变得更加复杂，可靠性也更难保证。然而垃圾收集过程中的任何错误或异常都会导致用户程序在运行时产生不可预测的结果。因此要确保用户程序的有效执行，势必对垃圾收集的可靠性和安全性进行严格地研究。JML是一种精确的形式化的行为接口规范语言，继

5、承了契约式设计的所有优点，能够规范程序模块的行为及详细设计决策，同时可以利用自身开发的工具进行高效率的测试，从而有效地保证软件质量。本文首先从垃圾收集技术的基本概念和基本技术出发，深入浅出地分析了垃圾收集技术背后的运行机理及其在具体内存堆上的行为，利用三色抽象原则实现了标记．清扫垃圾收集算法。为了减少垃圾收集给用户程序带来的停顿，在此基础上对算法进行改进，采用逐步更新的写拦截器实现了渐进式垃圾收集。为了严格地验证垃圾收集的安全性和正确性，本文首先利用Daikon动态分析工具和ESC／JAVA静态检测工具辅助生

6、成程序不变量，然后使用JML对垃圾收集与用户程序交互过程的安全规范进行精确描述，避免了使用自然语言产生的需求不精确、可能产生歧义的问题。本文通过JML运行时断言检测完成了垃圾收集和用户程序交互的自动化形式验证，证明了不可达节点的正确回收以及整个收集过程中内存堆的数据保持和用户数据的不变性，保证了用户程序没有干涉垃圾收集器的正确执行，同时也确保了用户程序数据未被垃圾收集修改。最后通过实际的例子对两种垃圾收集算法进行比较分析，结果表明渐进式垃圾收集器能够缩短中断时间并且降低内存需求量，有效地提高了垃圾收集的运行效

7、率。关键词：契约式设计；程序不变量；Java建模语言；垃圾收集；分类号：TP391文献标识符：AABSTRACTABSTRACT：Garbagecollectionhasbeenwidelyappliedinthefieldofmainstreamsoftwaredevelopmerit，whicheffectivelyavoidssecurityvulnerability,andimprovesres01】rceutilizationaswell．However，GCitselfiscomplex，itma

8、kesmoredifficulttoensurethereliabilityofthealgorithmdesignandimplementation．TheintroductionofmultithreadingtechnologywhichbringstoparallelexecutionbetweenGCanduserprogram，resuItsinmorecomplexinteractiv