Web应用是一种客户端(或用户界面)运行于一个Web浏览器上的软件应用。一个前端Web应用程序包括HTML页面、CSS样式文件以及相关的JavaScript脚本等。AJAX(Asynchronous Javascript And XML)是 Web 应用中异步调用的最普遍、最有效的实现,但异步调用的回调机制在增加客户端处理事务吞吐量的同时,会造成浏览器端和服务器端之间的并发缺陷。Web应用原子性违反是一类特殊的并发缺陷:原子区域被异步事件的回调机制打断的操作。异步事件的触发和回调执行在一个原子区域上的操作应该是连续的,而当这一连续的原子性操作间产生一个异步请求行为,使得当前异步事件和另一个异步事件的回调操作间的顺序变成不确定,最终影响输出结果,并可能造成商品超卖、系统崩溃等严重问题。现有研究通常采用静态分析方法进行Web应用原子性违反检测,具有高覆盖率的优点,但还存在精确度低、不能分析JavaScript动态特性等不足。为此,根据JavaScript的特性和动态分析框架Jalangi,我们实现了一种结合动态分析和约束求解的JavaScript原子性违反检测及定位工具AVChecker(Atomicity Violation Checker的缩写)。AVChecker包括5大模块:动态插桩、原子区域识别、原子性违反检测、事件建模和原子性违反定位,各部分功能如下:(1)动态插桩模块首先通过插桩记录数据流和控制流信息,然后提取Web应用程序中与JavaScript函数相关的一些元素信息,包括XHR对象、对应DOM调用的API、匿名回调函数等。(2)原子区域识别模块主要分析JavaScript函数的调用关系,包括回调函数的调用,然后识别出回调阶段完整的函数执行链,用于识别出三种类型的原子区域:HTML,CSS 和 JavaScript。(3)原子性违反检测模块首先构造活动间事件约束,包括事件间的原子区域约束和事件内的函数约束,然后对约束进行重新编码,再将SMT求解器作为求解工具来检测是否存在原子性违反。(4)事件建模模块主要将收集到的Trace中信息转换为一个完整的事件模型Aevent,包括对XHR对象的建模、DOM元素的识别和提取以及JavaScript 回调函数的处理。(5)原子性违反定位模块实现了细粒度的并发缺陷定位,即首先采用有限状态自动机表达AJAX的周期,并根据动态事件模型Aevent,设计规则将Trace转换成基于Aevent的Trace,再依据检测到的原子性违反结果定位到造成违反的Aevent 事件对 TAP。实验中的网站选自Alexa-top500,我们从中选取了 22个包含稳定原子性违反的网站。实验结果表明:AVChecker可以有效检测出Web应用中基于AJAX的原子性违反,误报率较低(18%);准确率可达到81.96%,好于现有的检测工具EventRacer,并且能检测出更多DOM类型的问题(175个VS94个)。定位实验结果表明我们算法的定位成功率达到84.5%。