一种基于程序不变量的合约式软件故障预警方法

摘要

一种基于程序不变量的合约式软件故障预警方法，（1）使用Daikon工具为需要预警的程序生成程序不变量，根据测试用例集在Daikon工具上运行源程序产生不变量，输出程序不变量；（2）筛选不变量；（3）手动生成由布尔断言组成的数据合约；（4）将上述步骤2和3中两种方式得到的合约以规格化进行表示，并将规格化表示后的所述合约以注释的方式插桩到源程序的相应位置；（5）将步骤4中插桩到相应位置的注释转换为具有故障检测性质的代码，并插桩到源程序的相应目标位置；（6）运行经步骤1至5处理后的源程序，如果程序运行过程中违反了程序合约，则故障检测代码会自动把监测到的故障展示给用户。

主权项

一种基于程序不变量的合约式软件故障预警方法，其特征在于：其包括如下步骤：(1)使用Daikon工具为需要预警的程序生成程序不变量，将需要预警的源程序和对应于源程序的测试用例集作为Daikon工具输入，根据测试用例集在Daikon工具上运行源程序产生不变量，输出程序不变量；(2)筛选所述不变量，所述筛选方式包括自动筛选和用户手动筛选，并将筛选后的不变量作为合约的一种来源；(3)手动生成由布尔断言组成的数据合约，所述数据合约是数据流的行为约束；(4)将上述步骤(2)和(3)中两种方式得到的合约以规格化进行表示，并将规格化表示后的所述合约以注释的方式插桩到源程序的相应位置；(5)将步骤(4)中插桩到相应位置的注释转换为具有故障检测性质的代码，并插桩到源程序的相应目标位置；(6)运行经步骤(1)至(5)处理后的源程序，如果程序运行过程中违反了程序合约，则故障检测代码会自动把监测到的故障展示给用户，表示有故障产生，并将整个运行过程中预警到的故障记录到预警日志中；所述规格化合约的类型包括方法前置条件和后置条件型合约、类不变量型合约、循环不变量型合约以及其他类型合约，所述循环不变量型合约用于找出在循环中出现的错误，且所述循环不变量型合约插入循环头及循环体之间，所述类不变量型合约为在整个类中保持不变的性质，类中每个方法调用时都要对该性质进行检查是否违反该性质，且所述类不变量型合约在类体结束处插入源程序。