多线程编程和异步事件处理的支持使得安卓应用的执行行为具有不确定性。若两个未经正确同步的事件对某一共享内存单元的访问可并发执行,且其中至少一个事件为写访问,则产生数据竞争。数据竞争是一种常见的并发缺陷,可导致安卓应用运行异常、崩溃、数据无效更新等严重后果。现有的安卓应用数据竞争探测技术一般采用动态或者静态探测方法,存在静态探测误报率高,动态探测代码覆盖率低、漏报率高等问题。为提高安卓应用数据竞争探测能力,本文提出一种基于约束求解的安卓应用数据竞争探测方法。该方法首先采用静态分析技术获取共享变量访问、冲突事件对等信息,生成所有的潜在数据竞争;然后采用动态搜索技术生成待测应用的GUI测试模型,采用符号执行技术生成待测应用的符号摘要信息,针对潜在数据竞争事件,基于GUI模型和符号摘要信息生成可覆盖相应潜在数据竞争代码的候选事件序列;最后动态运行各候选事件序列,收集各事件序列的执行轨迹,并采用基于约束求解的预测性分析技术,对执行轨迹中可能产生数据竞争的事件对进行约束求解,将并发错误探测问题转化为约束求解问题。该方法通过静、动态分析收集并执行多个候选事件序列,克服动态探测方法中代码覆盖率低等缺陷,同时保持了预测性分析技术误报率低、效率高等优势。在上述工作的基础之上,本文设计并实现了基于约束求解的安卓应用并发错误探测工具ADR,并与动态数据竞争探测工具Event Racer和静态数据竞争探测工具n Adroid进行对比。实验结果表明,ADR可有效探测安卓应用中的数据竞争,在探测效果和效率之间达到了一个较好的折中。与Event Racer相比,ADR通过生成多个事件序列提高代码覆盖率,可探测出更多的数据竞争;与n Adroid相比,ADR提高了探测精度和效率,探测时间减少约67%。