随着信息社会的发展，计算机软件已渗透到日常生活的各个方面，提高计算机软件的可靠性和安全性，以保证其按照人们期望运行的要求变得十分迫切。现有的软件质量保障技术主要包括软件测试、程序分析、模型检测等，但这些技术无法保证最终部署在实际系统上的程序运行时是无错误的。运行时验证（RuntimeVerification）是一种新兴的轻量级验证技术，它把形式化验证技术和系统的实际运行结合起来，监控系统的实际运行，以保证系统的运行与系统关键性质相一致。在运行时验证中，监控器持续监控程序的运行，以判断程序的当前运行轨迹是否满足或违背监控性质。基于面向方面编程技术（Aspect-Oriented Programming，AOP）的软件运行时验证把针对软件的运行时验证当做一个横切关注点来对待，提高了被监控软件系统的模块化程度。由于AOP技术能够把软件运行时验证关注点模块化，同时AOP语言中接入点模型很直观的对应于软件运行时验证中监控事件，基于AOP的软件运行时验证技术在研究界和工业界得到了广泛应用，当前主流的运行时验证框架，如Tracematches，JavaMOP都是基于AOP语言的。随着被监控软件规模增大、并处于不断演化之中，同时运行时验证技术的应用范围在扩展，用户对运行时验证技术检测出问题的时效性也在增强，由于基于AOP的监控器以一种obliviousness方式注入到被监控程序中去，还往往可以对被监控程序进行任意调整，这些都给用户清晰、正确地使用基于AOP的运行时验证技术带来挑战。本文以帮助用户正确、高效使用基于AOP的软件运行时验证技术为目标，提出了一系列语言、方法和技术，帮助用户正确地指定其要监控的性质以及检查针对某一具体程序生成的监控器是否准确反应了用户的监控期望。本文的主要研究贡献包括：1.针对当前基于AOP运行时验证框架提供的事件序列语言不加区分的使用AspectJ中切面语法和不能根据事件间数据流关系选择事件序列的问题，提出了一种运用于软件运行时验证的事件序列选择语言。该事件序列选择语言通过一个受限的切面语法选择单个事件，并有着清晰的层次结构：低层操作符完全通过事件发生的局部环境选择单个事件；高层的操作符利用事件间的控制流和数据流关系选择事件序列。同时，该事件序列语言支持数据流声明，与目前主流的运行时验证框架提供的事件序列选择语言相比，该语言能够表达更细粒度的事件序列。2.针对现行运行时验证中监控事件逐个到达的假设和用户期望更早发现被监控程序的运行是否违背监控性质间的矛盾，提出了面向于运行时验证领域的预测语义。当前的软件运行时验证技术大多都基于监控事件逐个依次到达的假设，这使得监控器只能在故障发生时才能对程序进行调整。如果结合对被监控程序进行静态分析，尽可能多地找出被监控程序运行过程中会产生的监控事件串（序列），这样可以使监控器更早地发现被监控程序的当前运行能否满足或违背监控性质，从而可以对故障进行预测，使用户能够更灵活地进行调整。我们对这种方法进行了形式化的定义，并提供了工具支持。我们使用该工具在几个大型开源项目上进行实验，结果表明带预测语义的运行时验证具有一定的实用性。3.针对基于AOP的运行时验证框架中由于事件选择语言的复杂性引起的性质层面监控器和实现层面监控器间的不一致性以及同一被监控程序上部署的多个监控器相互干扰的问题，提出了基于AOP的监控器内部和监控器之间存在的冲突及相应的检测算法。在基于AOP的软件运行时验证中，由于选择监控事件切面的复杂性，用户在定义监控器时可能会出现在性质层面明确的监控器在实现层面不明确，使得最终生成的监控器没有正确反映用户的监控需求。同时在被监控程序中存在多个监控器注入的情况下，各个监控器间可能互相影响，使得监控器无法依据监控性质正确检测被监控程序的最终运行。针对这些问题，本文第五章对此定义了AOP监控器内部和监控器之间的冲突并提出了相应的自动检测算法，这些定义和检测方法能够帮助用户及时发现监控器中存在的问题，更清楚地掌握其定义的监控器和监控器在被监控程序上的使用。4.针对往被监控程序中注入监控器有可能破坏被监控程序原有重要性质的问题，根据监控器对被监控程序原有性质的影响提出了关于监控器的一个分类框架及自动检测方法。由于当前基于AOP的运行时验证框架允许用户在被监控程序的运行满足或违背监控性质的情况下对被监控程序进行任意调整，这有可能会破坏被监控程序的原来保持的某些重要性质。对此，本文第六章根据监控器对被监控程序原有性质的影响提出了一个基于AOP运行时监控器的分类框架。同时，还根据各种不同类型监控器所具备的一些典型代码特征给出了一个监控器类别检测算法。该分类框架和类别检测算法有助于用户选择正确的监控器和掌控对监控器的使用。