论文部分内容阅读
随着软件在社会生活应用中的不断深入,软件系统的体积和复杂度都呈现出迅速增长的态势,软件可靠性问题也相应成为软件行业发展不容忽视的重要方面。在现有的软件验证技术中,运行时验证作为一种轻量级的验证技术,综合了运行时监控技术和形式化规约技术,是当前软件验证领域的一个研究热点问题。而在运行时验证的技术实现中,一方面需要实现待验证性质的描述和相应验证器的生成,另一方面需要将监控器和验证器集成到待监控的软件系统中,即监控和验证代码的插桩。由于软件体积和复杂度的不断增加,基于日志API监控或手动进行监控验证代码插桩明显不能满足不同平台,不同类型系统监控验证的需求。随着编译器技术和面向方面编程技术的不断发展,利用编译器实现代码自动插桩,借助面向方面语言实现插桩位置描述和模块化管理,正在成为推动运行时验证实际应用的重要研究领域。本文分析了C语言的编译流程,LLVM开源编译器框架及其Clang编译器前端,在此基础上参照面向方面编程的概念,设计并实现了一种针对C程序的面向方面语言MOVEC,其相应编译器能够解析监控器插桩位置的描述并利用源代码插桩技术实现插桩需求。同样基于源代码插桩的技术,本文设计并实现了软件中除0,整数溢出和变量使用前未初始化错误验证器的插桩。通过将MOVEC语言编译器和现有针对C/C++程序的面向方面语言编译器AspectC,Aspect C++在准确性,插桩时间,程序性能影响和程序代码膨胀等方面进行对比,表明MOVEC语言能够在保证对程序性能的低影响前提下,实现更高的准确性,更低的插桩时间,更小的代码膨胀率。实验同时验证了三种常见错误验证器设计和插桩方法的正确性。本文的工作为运行时验证监控器和验证器插桩的自动化,高效率,跨平台实现提供了基础,能够促进运行时验证在实际生活中的应用。