一种针对软件模型检查工具的测试用例自动生成方法和系统

摘要

本发明公开了一种针对软件模型检查工具的测试用例自动生成方法，所述方法包括如下步骤：使用Clang编译器前端对待测试的源代码进行分析，根据分析结果插入用于记录程序运行状况的桩语句，不改变程序原本的逻辑；编译并运行程序，获取程序运行过程中的状态；对源程序进行处理，将程序实际的运行状态作为待检查的条件判断，嵌入源代码产生测试用例；以所述得到的测试用例运行软件模型检查工具，得到检查工具在该测试上正确与否的结果。本发明还公开了实现上述方法的系统。本发明能够根据已有的程序源代码自动生成适用于软件模型检查工具的测试用例，能够自动化地发现相关工具中隐藏的软件缺陷。