软件运行时验证加速中的多目标约束模型研究

摘要

In the process that to test whether the lightweight formal verification method satisfies the givn properties,it often produces high time overhead,which hiders the application of this technique in deployed systems.In this paper,by identifying inherent dependencies among multi-objective constraint of runtime verification,a decision equation was constructed to decide that which is optimizable monitor,and this decision equation can be considered as a multi-objective constrained model for speeding up runtime verification.Experimental results show that this model is capable of deciding that which is optimizable monitor,and provides a quantitative basis for speeding up runtime verification.%通过监控程序运行检验软件运行是否满足给定性质的轻量级验证中常产生高额的时间开销，阻碍了该技术部署后在系统中的应用。如何减小验证开销、提高验证效率，已成为亟待解决的难点问题；通过识别运行时验证优化过程中多目标约束间的内在依赖关系，定义并构建了可加速监控器的判定方程，作为验证加速的多目标约束模型。实验表明：该模型的求解结果能够用来判定哪些是可加速监控器，为实施软件运行时验证的加速提供量化依据。