一种基于约束求解的原子集合序列化违背探测方法

摘要

本发明公开了一种基于约束求解的原子集合序列化违背探测方法，属于软件测试技术领域。该方法包括如下步骤：首先动态收集并发程序原始执行轨迹，然后结合原子集合序列化违背的九种错误模式，建立原始执行轨迹中相关事件之间执行先后顺序的约束关系，将原子集合序列化违背的探测问题转化为约束求解问题，并利用Z3求解器进行约束求解，当约束有解时，该解对应的可执行交织中存在原子集合序列化违背错误，否则不存在。本发明扩大了原始执行轨迹中事件的交织空间，同时保证了由约束求解所生成的交织是可行的，由此降低了原子集合序列化违背探测的漏报率和误报率，提高了原子集合序列化违背探测能力。