基于预测的开销可控运行时验证技术研究

摘要

软件运行时验证作为一种新兴的软件质量验证方法，区别于传统的软件测试和模型检测，能够避免状态爆炸问题以及测试用例不完备的问题，这一特点使得运行时验证技术越来越受到关注。然而由于运行时验证是基于对软件系统进行实时监控进行的，监控行为在多方面对软件运行效率造成了影响。本文针对这一问题，提出了一种基于预测的开销可控软件运行时验证方法。基于对软件历史运行数据的处理和分析，研究出软件运行规律，并以此预测软件未来运行风险。当运行时验证对目标系统的运行效率产生的影响不可忽视的时候，软件未来运行风险可以指导运行时验证系统对自身的监控行为进行自我调控，从而维持软件本身的正常运行。
　　本文的主要工作如下:
　　1.在对现有的运行时验证技术进行研究的基础上，提出了基于预测的开销可控软件运行时验证框架。该框架对传统的运行时验证流程进行改进，加入了改善运行时验证系统运行效率的手段。该框架首先通过PEDL和MEDL脚本语言完成对目标系统的插桩，然后收集软件的历史运行数据，对其进行分析，利用马尔科夫链和隐马尔科夫模型进行软件未来运行风险评估，最后根据风险评估的结果对软件监控行为进行调控，并将这些内容与MaC框架进行结合。
　　2.提出了根据软件运行历史信息来预测软件未来运行风险的方法，分别使用马尔可夫链和隐马尔可夫模型，针对对软件中对系统中所有状态都为可观察状态以及系统中包含部分隐含状态的情况给出解决方案。首先给出根据历史数据建立软件行为模型的方法，然后根据模型给出未来有限步数内，针对某一性质的软件行为的运行风险的计算方法。并在此基础上，给出了根据软件运行风险进行监控行为调控的策略。主要采用代码版本控制的手段，利用对监控行为的实时控制，实现有侧重的监控，并最大程度的保证软件监控的效果。
　　3.在上述理论研究成果的基础上，设计并实现了基于预测的开销可控软件运行时验证原型工具PCRV。在此基础上，将原型工具运用到案例中，并且对监控开销控制进行了实验，分析实验结果，证明了本文所提的运行时验证框架在提高验证系统运行效率中的作用。

目录

封面

声明

中文摘要

英文摘要

目录

第一章 绪论

1.1 研究背景

1.2 国内外研究现状

1.3 本文的主要工作

1.4 论文的组织结构

第二章 研究基础

2.1 运行时验证相关概念和技术

2.2 MaC验证框架

2.3 马尔可夫链

2.4 隐马尔可夫模型

2.5 自动机理论基础

2.6 本章小结

第三章 基于预测的开销可控软件运行时验证方法

3.1 基于预测的开销可控软件运行时验证基本框架

3.2 软件行为信息的收集和概率模型的建立

3.3 软件行为风险预测方法

3.4 运行时验证开销控制策略

3.5 监控器构造方法

3.6 本章小结

第四章 运行时验证工具实现

4.1 验证工具的输入与完成目标

4.2 工作流程和总体框架

4.3 主要功能模块的实现

4.4 本章小结

第五章 案例及实验分析

5.1 性质规约以及监控器构造

5.2 事件条件定义及代码插装

5.3 程序运行时验证过程

5.4 监控功能的控制

5.5实验及结果分析

5.6 本章小结

第六章 总结与展望

参考文献

致谢

在学期间的研究成果及发表的学术论文