论文部分内容阅读
随着软件规模和复杂度的迅速增长，软件质量管理在整个软件开发周期中的作用受到越来越广泛的重视。软件验证是保证软件质量的主要方法之一。常见的软件验证方法包括静态分析、动态测试及运行时验证等。运行时验证是一种动态方法，既可以应用于离线的软件测试过程，又可以应用于已经上线的软件系统。由于运行时验证可以获得运行时刻的数据、监测真实的系统行为，因此可以有效的检验出一些传统方法难以发现的缺陷。
基于约束的验证是软件验证的一种重要形式，其基本思想是描述软件必须遵守的约束，并对这些约束进行验证。本文主要关注应用程序接口（ApplicationProgramming Interface：API）使用约束的描述及其运行时验证。在软件开发过程中，开发框架或者较底层的软件通常会提供一些API供上层应用调用，例如Java开发工具包。当上层应用调用这些API时，通常需要遵守某些API使用约束，以获得正确的运行结果。违反这些使用约束将导致不同类型的系统缺陷。现有的研究大多关注于单个对象上的API使用约束的描述和验证，而本文则致力于对涉及多个对象的API使用约束进行描述，并采用动态方法对其进行运行时验证。
本文主要有如下贡献：（1）提出了一种多对象API使用约束的描述语言LACOIO（Specification Language for API Constraint on Multiple Interacting Objects），用于形式化的描述此类约束，使得此类约束可以自动的被计算机理解；（2）一个LACOIO编译器，用于将约束描述文件自动编译成验证代码，这些代码将被自动部署到被验证的目标应用上；（3）一个运行时验证框架，对目标应用进行验证，在运行时刻检查其是否违反己定义的约束；（4）一组运行时验证的性能优化策略，用于降低验证造成的开销。
本文的评估结果显示，LACOIO的描述能力高于现有的一些描述方法，且其编译器和运行时验证框架具有较好的性能。