多目标约束下软件运行时验证加速技术框架

摘要

软件运行时验证是一种近年来逐步兴起的通过监控程序运行来检验其是否满足给定性质的轻量级验证技术。由于复杂性质的运行时验证中常产生高额的时间开销，阻碍了该技术在部署后系统中的应用。在深入剖析国内外研究现状及存在问题基础上，从改善部署后软件运行时验证效率的角度出发，综合考虑性质违背检测能力、诊断支持能力等潜在开销优化制约因素，提出多目标约束下的软件运行时验证加速技术框架。该框架包括构建多目标约束模型、可加速监控器判定、加速控制技术研究以及原型工具开发等内容，并具体阐述了框架所涉及的关键技术方案。本研究将为解决运行时验证中的开销问题提供关键技术支撑，为运行时验证技术在部署后系统中的工程化应用奠定基础。%Runtime verification is a relatively new lightweight formal verification method which is concerned with dynamic monitoring and analysis of system executions with respect to precisely specified properties.Runtime verification of complicated properties that involve many system variables imposes high overhead,which makes it is hard to apply this method in the context of deployed systems.This paper considered all the latent constraints including the efficiency of property violation detection and fault diagnosis.It involved the key technology at the topic of speeding up for runtime verification on the condition of multi-objective constraint.It mainly includes:to construct a model of multi-objective constraint,to resolve the problem of how to recognize the involved monitor for speeding up by constructing heuristic algorithm to get the answer for multi-objective model on the basis of monitoring statistics information of verified systems before speeding up,using control theory,to implement runtime verification speeding up by constructing self-adaptive speeding up control algorithm.This research will provide key technologies for resolving the overhead problem of runtime verification.And it can also provide a basis for applying the runtime verification method for actual deployed systems.