针对软件测试和静态程序验证中存在的连续性程序执行验证和推理问题,提出一个基于程序插桩和布尔逻辑的运行时程序验证框架——RPA。定义一种用于描述运行时程序性质和规范的动态逻辑语言RPAL,实现自动化插桩以收集运行时程序状态信息,设计一个支持高效验证的句子调度算法。实验结果表明,结合合适的谓词扩展,RPA可以有效地验证和分析软件逻辑,发现潜在的软件错误。
Continuously verifying and reasoning on software's execution property are notoriously hard to solve by general software test and static program verification.Aiming at the problems,this paper proposes a runtime program verification framework named RPA based on program instrumentation and Boolean logic.RPA defines a dynamic logic language which describes and asserts runtime properties of target program,proposes an automatic instrumentation approach to collect state information in runtime program,and designs a scheduling algorithm to support fast verification and reasoning.Experimental results show that combined with appropriate predicate extensions,RPA can effectively verify and analyze the software logic,to identify potential software errors.