面向对象编程(Obiect-Oriented Programming,OOP)是一种实现软件模块化和可重用的编程规范,较好地解决对象和数据的封装问题。但是随着编程实践的日益丰富,OOP也表现出缺陷:在加入横切关注之后的代码容易产生交织、分散问题,使得代码难以理解和维护。面向切面编程(Aspect-OrientedProgramming,AOP)方法应运而生,为上述问题提供了一种有效和可行的方法:AOP支持软件模块化和可重用,能有效地消除代码的交织和分散问题。AOP将程序被描述成对象和切面的集合,通过织入器把切面织入到程序中。由于切面如何描述在很大程度上影响到系统的关键行为(比如性能和同步),与此同时,系统的关键行为使得切面的描述复杂化,Bugs可能存在于程序中而难以发觉。因此AOP程序的验证工作相对复杂。我们需要一种方法来测试或验证AOP程序的正确性。目前对AOP的研究侧重于语言本身的实现和应用,而对程序进行检查和验证的相关研究十分缺乏。针对目前的需求,本文提出一种基于运行时验证的框架来检测AOP程序,使得AOP程序中横切关注点的验证得以实现。在这种框架中,程序的性质由线性时序逻辑公式描述,并在程序执行时使用运行时验证技术来验证。本文给出该框架的整体流程和核心算法,并使用一个详细的案例对研究内容进行分析介绍。