一种针对源代码的运行时形式化验证方法

摘要

本发明公开了一种针对源代码的运行时形式化验证方法，根据源程序所需满足的性质以及工具所需参数编写用于生成监视器与切面类的配置文件；根据编写的配置文件使用运行时验证工具自动化生成监视器以及切面类；根据生成的切面类将所涉及的变量置入源程序；修改仿真内核以适用于运行时验证方法；使用生成的监测器对插桩后的源程序运行状态进行实时监测；监测器根据程序运行的轨迹对性质进行形式化验证，若出现违反验性质的路径，则记录或者进行程序的自动修复。本发明所述方法可以应用到嵌入式系统及大型软件系统的形式化验证中，能够提高软件的安全性、可靠性。