基于AOP的运行时验证中的冲突检测

Conflicts Detection in Runtime Verification Based on AOP

现有的形式化验证方法除了在模型层面对系统进行验证以外,越来越倾向于直接针对系统的实际代码和具体运行.运行时验证技术验证的对象是具体程序,它试图把形式化验证技术部署到程序的实际运行过程中.然而在把形式化技术部署到实际运行过程中会出现一系列在模型层面验证通常不会出现的问题,对这些问题中的冲突现象进行了研究,定义了运行时验证技术中存在的两种冲突,并给出了相应的检测算法.最后,对这些算法进行了实现和实例研究,结果表明了该方法的有用性.

Nowadays,instead of only verifying systems at the model level,current state-of-the-art verification techniques tend to focus on real code and real system’s execution.Runtime verification checks the system’s execution and tries to bridge the gap between formal verification techniques and real systems.However,this brings about some problems which usually do not appear in model-level verification.This paper analyses the problem in runtime verification.It defines two kinds of conflicts and lists their corresponding detection algorithms.These algorithms are implemented based on an open source runtime verification tool and some real cases are examined.The results demonstrate the effectiveness of the proposed method.