，

(1. 河北科技师范学院工商管理学院，河北秦皇岛066004；2. 燕山大学信息科学与工程学院，河北秦皇岛066004)

移动设备大多资源受限，为了能在其上流畅运行具有丰富功能的应用程序，Android等主流平台广泛采用了多线程等技术，有效降低了应用程序的响应延迟并提升了其并发执行性能。与传统应用程序的多线程模型不同，Android系统采用事件驱动模式，各种来源的输入(比如UI、网络、传感器和Android生命周期等)都有可能触发事件，使多线程模型中执行的任务按某种规则以不确定的方式重新排序。这些复杂的并发特征容易产生数据竞争[1-3]等并发错误，纠错十分困难。

传统的数据竞争检测技术[4-10]，提供了许多有益的建模理论和检测方法，但并不适用于Android Apps多线程模型的数据竞争检测。针对Android Apps的数据竞争检测，学者们发展了静态检测[11-16]和动态检测[17-18]的技术。文献[11-12]采用新颖的方法对移动应用程序进行数据竞争检测，但没有考虑事件回调之间的happens-before关系，影响了其检测精确度，同时存在大量误报问题。SUN等[13]通过重放技术有效降低了误报率。HU等[14]对并发动作及其时序关系进行建模，在降低误报率的同时提高了检测效率。FU等[15]提出了将事件回调之间的时序关系转换为线程间的时序关系的线程化技术，大大降低了误报率。WU等[16]提出一种流和上下文敏感的时序分析方法，可以检测线程内和线程间的数据竞争问题。但静态检测技术固有的状态空间爆炸问题，难以突破检测效率低的瓶颈，使得其实用性不足。文献[17-18]采用动态检测技术，通过采集Android Apps的执行路径信息，基于happens-before关系进行离线检测，检测效率高但代码覆盖率低，存在大量的漏报问题。因此，如何在多线程和事件驱动的Android平台上精确描述和分析Apps中的并发行为，提高模型精确性的同时不牺牲模型的效率，是Android Apps行为建模与检测研究过程中亟待解决的关键问题之一。

本文针对事件驱动机制下多线程模型的安全问题，构造一个基于Pi演算的并发行为检测模型，并利用该模型对Android Apps中的数据竞争问题进行检测。

1 数据竞争问题

图1给出一个利用AsyncTask加载数据的示例AsyncApp。应用程序启动时，主线程创建一个后台线程执行加载数据的异步任务。为了良好的用户体验，后台线程持有MainActivity的引用并使用一个进度对话框(ProgressDialog)显示加载的进度信息。待加载任务完成，后台线程将加载数据返回到主线程用onPostExecute方法显示出来，主线程调用对话框的dismiss方法撤销对话框资源。如果用户在数据加载过程中触发后退操作(点击导航菜单上的后退钮)，则MainActivity被销毁导致状态丢失。但AsyncTask还持有MainActivity的引用，待异步任务返回onPostExecute，进度对话框调用dismiss撤销对话框资源会引发NullPointer Exception异常。

图1 AsyncApp程序示例代码Fig.1 A motivating example of AsyncApp

由于主线程和后台线程共享MainActivity数据，构成了数据竞争关系。UI事件(如点击导航菜单上的后退钮、旋转屏幕等)和应用程序的回调事件并发，使得MainActivity的onDestroy和主线程的onPostExecute执行时序不确定，产生了数据竞争问题。

可见，若共享的资源、程序片段被多个方法操作，且其中至少有一个执行的是写操作，则多个方法执行次序的不确定就会引发数据竞争问题。

上例中，若onPostExecute总是先于onDestroy执行，则不会发生异常。但Android是事件驱动的系统，UI事件由用户随意触发导致了时序的随机性。针对该问题，一种简单的解决办法是在使用共享数据之前进行判断，称为条件护卫原则。如图1中onPostExecute方法里注释的if语句，但并不能保证App的开发者总能遵循该原则，因此需要发展一种自动进行检测的方法。

2 扩展Pi演算

由于进程代数[19-20]可以有效描述并发行为和消息通信特性，本文将其中的Pi演算[21]作为建模语言，并对其进行扩展，使之适合描述Android Apps且利于编码实现。下面给出扩展后的Pi演算的语法和语义规范，定义如下。

经过扩展的Pi演算同时具备描述移动性、外部接口通信和内部状态迁移的能力，适合形式化地表示Android应用程序的执行路径和组件间通信的情况。

将进程P所有的行为迹组成的有限集合记为Ptraces。

定义2迹等价(trace equivalence)。给定两个不同的进程P和Q，称进程P和Q是迹等价的，当且仅当Ptraces=Qtraces成立。记为P≈tQ。

定义3α变换(alpha conversion)。将进程中的名字换成新的名字的变换称为α变换。

一般来说，用于替换的新名字应为进程中原来不存在的名字，若该名字已存在，则须变换进程中的名字，以保证不会出现命名冲突。使用符号{b/a}P表示将P中的名字a替换为b。如P=υba.b，则有{c/a}P=υbc.b，{c/b}P=υca.c，{b/a}P=υb′b.b′。

选定了进程等价定义，就可以确定出相应的迁移规则。最常用的几条迁移规则如下。

(F) SC-RES-COMPυx(P1‖P2)≡P1‖υxP2，若x∉fn(P1)

3 形式化建模

与传统的应用程序不同，Android Apps并不是独立的封闭程序，需要在Android框架中运行。Android系统(包括Android运行时环境)在应用程序的代码之外做了大量的工作。其中，Android系统为了管理应用程序，为每个组件预先定义好生命周期，应用程序可以为生命周期定义回调函数和监听函数。因此，为了得到更精确的模型，需要为Android生命周期构建形式化模型。

3.1 Android生命周期的形式化建模

以Activity组件的生命周期[22]为例，根据拓展Pi演算的形式化语法和语义，得到模型如下。

上述进程表达式中的τ为不可见动作，在这里指代不可预知的事件。其他组件(Service和Fragment等)生命周期的形式化模型构造方法与Activity组件相同，不再赘述。将这些组件的生命周期并发演算，得到Android Apps的生命周期的形式化模型。

3.2 多线程的形式化建模

当Apps启动时，系统会为其创建一个主线程(main thread)来负责和UI组件进行交互。若某个操作比较耗时，就可能阻塞主线程而导致交互卡顿。Android系统主要通过HandlerThread、AsyncTask和线程锁Lock等机制解决这个问题。

Android中实现多线程的方式有两种：(a)继承Thread类，并重写类中的run()方法，但一个类只能继承一个父类；(b)实现Runnable接口。无论哪种方式实现，都会出现类似thread tr=new thread(…)和tr.start()的两条语句。因此，按如下步骤进行形式化映射。

分析thread tr=new thread(…)类似语句及其上下文，确定新建线程tr的类名称son和线程类所在基本块。在这条语句的上文搜索，若出现P：son implements Runnable语句，则说明线程是通过实现Runnable接口实现的；若出现P：son extends Thread语句，则说明线程是通过继承Thread类实现的。其中P表示基本块的编号(标记了线程类所在基本块)，son表示线程类的名称，在实际分析中会以具体的值出现。

下面给出线程的映射规则，如图2所示。新建线程实例tr的线程类名称为son，对应的基本块编号为S。线程类定义了该类线程实例的行为模式。因语句tr.start()执行后线程实例tr就会和father线程实例并发执行，所以在动作start后添加同步动作son(son线程类的地址)，并将其作为同步并发的通道。father线程的实例将start语句所在基本块的地址(用新名字p表示)通过son通道传送过去。线程类son的实例通过son通道接收p并将其存储到l中，两个线程开始并发执行。

这个过程，可以形式化地描述如下。

其中，子线程son的进程S可能会产生多个，因此使用了复制算子。按照扩展Pi演算的操作语义，father线程和son线程进行并发演算，在使用了COMM-L、CLOSE-L等规则之后，经过(newthread，start，τ(son))一系列动作后，father线程和son线程开始并发执行。经过这样的映射，形式化地表示了父子线程间的并发特征。

图2 多线程的映射规则Fig.2 Mapping rules of multithread

3.3 并发特征分析

下面以AsyncTask为例进行并发特征分析。

AsyncTask是Android提供的一个轻量级的异步任务处理的工具类，其时序图如图3所示。在执行后台耗时操作之前，AsyncTask在主线程里执行onPreExecute进行一些初始化操作，然后在后台线程里执行doInBackground方法处理那些耗时任务。一旦任务执行完毕，主线程就会调用onPostExecute方法将结果返回到主线程并更新UI界面。其中publishProgress方法运行在后台线程用于更新任务进度，更新完成后主线程会执行onProgressUpdate方法展示任务进度。

图3 AsyncTask的时序图Fig.3 Sequence diagram for AsyncTask

图3中的几个方法都被重写，因此需要根据扩展Pi演算语法对这些过程间调用方法进行映射。如对于onPreExeCute的映射结果如下所示。

从映射结果可知，主线程的进程表达式PUIthread在和后台线程的进程表达式Pworkthread并发演算之前，需要先和onPreExecute方法的进程表达式PonPreExecute并发演算，即主线程在位置ps处调用onPreExecute方法并将ps发送给onPreExecute方法所在地址并存储为pr，等到onPreExecute方法调用结束后再通过pr返回。

线程间的关系主要是交互关系和时序关系，可以在线程间构造一些交互通道，巧妙地描述出这些关系。如主线程执行完onPreExecute方法之后，后台线程才能够执行doInBackground方法。为了描述这种时序关系，构造一个通道t1，主线程在执行完onPreExecute方法后，由通道t1向后台线程发送一个空消息，后台线程在doInBackground方法之前插入通道t1，保证只有在t1上接收一个消息后才能执行doInBackground方法，这样，就描述出了线程间的时序关系。对于交互关系，如publishProgress方法会把任务进度消息发送给onProgressUpdate方法，它们之间通信的通道在程序里没有体现出来，因此，也为它们构造一个通道i1，通过该通道传输任务进度消息。于是可得到如下映射结果。

PAsyncTask=υt1t2i1i2(PUIthread‖Pworkthread)。

其中并没有对后台线程Pworkthread使用复制算子，因为异步任务的线程一般只能被执行一次。由于用到了doInBackground方法中定义的publishProgress，所以给出了doInBackground的过程间调用的映射。但为了突出本文研究的问题，其他方法的过程间调用的映射被省略。

由扩展Pi演算的迁移规则可知，PAsyncTask经过路径(onPreExecute,τ(t1),τ(doInBackground), publishProgress,τ(i1), [onProgressUpdate, publishProgress],τ(i2),[ onProgressUpdate,τ(ds)],τ(t2),onPostExeCute/onCancelled)后成功终止。其中“[ ]”里的动作可能会以任意次序发生，如[onProgressUpdate, publishProgress]表示其路径可能是(onProgressUpdate, publishProgress)或是(publishProgress, onProgressUpdate)。“/”表示两个动作只能取其一，如onPostExeCute/ onCancelled表示要么onPostExeCute执行，要么onCancelled执行，但不会都执行。可见，本映射方法准确地描述了AsyncTask的并发特征。

4 并发行为检测

进程表达式描述了系统的行为模式，而系统需满足的安全约束则可用演算规则和迁移规则来描述。安全约束是指保证提供某种安全保护所必须遵守的规则。如为了保证多线程模型的时序安全，doInBackground方法必须在onPostExecute方法之前执行，该规则就是一条安全约束。

本文用包含进程表达式的IF-THEN规则表示演算规则和迁移规则，这意味着行为模式和行为所需满足的安全约束之间可以演算和迁移，达到自动分析和检测的目的。

4.1 规则构建

演算规则2(同步阻塞) IFa∉A，x∈A，THENa.P‖x.Q=a.(P‖x.Q)。

其中0表示故障停机。规则1、2表明，同步动作必须与其补动作同步执行而不能单独执行，且可以同步时必须优先执行同步动作。规则3表明，若一个系统中当前可执行的动作皆为同步动作且不互补，则会导致故障停机，发生同步异常错误。

演算规则4(异步演算) IFa,b∉A，THENa.P‖b.Q=a.(P‖b.Q)+b.(a.P‖Q)。

规则4表明，一般动作(不属于同步集A中的动作)以不确定的方式异步执行。这种不确定性导致异步演算中的并发进程最终能转换为和进程。

以上4条规则可容易地利用进程等价(定义2)进行证明，不再赘述。根据扩展Pi演算的语法和语义，利用这些演算规则可得到如下安全约束。

由约束2可知，可以提取出各种时序关系并通过比对Android Apps的进程表达式的时序，检测应用程序中存在的缺陷。还可以依据这些时序重写进程表达式，并在运行时检测应用程序中的API序列是否满足这些时序关系，从而判定行为是否正常。

利用安全约束1和安全约束2，可将相关研究中的happens-before关系[13-18]形式化地构造成IF-THEN规则，这样就可以复用这些成果，提高模型的精确性。

根据上面给出的演算规则，还可以推导出更多的演算规则。如由规则1和规则4可知，

由规则4可知，

IFa,b,c,d∉A，

THEN (a.P+b.Q)‖(c.R+d.S)=a.(P‖(c.R+d.S))+b.(Q‖(c.R+d.S))+

c.((a.P+b.Q)‖R)+d.((a.P+b.Q)‖S)。

接下来，给出迁移规则。根据和进程的定义，容易得到其迁移规则。

由和进程的迁移规则可知，迁移动作必须是和进程中某项的前缀动作，否则将无法进行迁移而发生异常，表述如下。

由和进程的迁移规则和演算规则可以推导出其他的迁移规则。如由演算规则1和5可知，若存在x∈A，则有

结合演算规则1和安全约束1，可得同步迁移规则。

结合演算规则2、4和安全约束2，可得到异步迁移规则。

由同步迁移规则可知下面情况无法迁移，会发生异常。

构建了并发行为的运算规则后，就可以据此进行行为检测，判定Android Apps中是否存在可能导致同步异常、迁移异常以及数据竞争等违反安全约束的行为。

行为检测的大体思路是：依据演算规则和迁移规则，由输入信息驱动进程表达式进行演算和迁移。本文模型将静态检测和动态检测相结合，静态检测模块将需要满足的规则作为输入，驱动模型执行检测；动态检测模块在目标App运行时，获取其API调用和触发事件(生命周期事件、UI事件)序列、Activity栈等信息作为输入，驱动模型执行检测。动、静态检测的输入虽然不同，但检测算法和步骤是相同的。

4.2 行为检测算法

为了在行为检测过程中记录进程表达式演算和迁移的状态，为每个App维护一个行为状态集asSet，由演算状态集calcSet和迁移状态集tranSet组成，即asSet::={calcSet,tranSet}。演算状态集记录当前演算前后的进程，即calcSet::={(oldprocess, newprocess)}。迁移状态集记录当前迁移到的进程和位置，即tranSet::={(process,{location})}，其中location可能有多个。

初始化演算状态集calcSet的方法描述如下：

(ⅰ)初始化calcSet为空；

(ⅱ)将目标App的进程表达式app_proess作为一个演算前进程添加到calcSet，即calcSet={(app_proess,NULL)}。

初始化迁移状态集tranSet的方法描述如下：

(ⅰ)初始化tranSet为空；

(ⅱ)使用GetFirstActions(app_proess)获取目标App的进程表达式app_proess中所有可能的首个前缀动作，并将其添加到tranSet。若app_proess中所有可能的首个前缀动作为a、b和c，则tranSet= {(app_proess,{a,b,c}}。

检测过程中，每次演算或迁移都更新一次asSet，更新算法如算法1所示。

算法1更新行为状态集asSet。

Input: API调用和触发事件序列、Activity栈等信息(动态检测)；需满足的规则，分为进程表达式和包含进程表达式的IF-THEN规则(静态检测)。

Output:行为状态集asSet。

Procedure:

1: Pe Cp,Rp,P,Q

2:action[] actlist, act

3:algorithm *alg, *algo

4:int algotype //1为演算算法，2为迁移算法

5: while Input!=NULL do

6: actlist=GetAPIEventSequence (Input)

7: Cp=GetprocofActivity(GetActivity(Input))

8: Rp=GetprocofRule(Input)

9: alg=GetalgorithmofRule(Input)

10: algotype=GetalgotypeofRule(Input)

11: if algotype==1 then //演算

12: if alg!=NULL then

13: asSet.calculation(alg)

14: end

15: if Rp!=NULL then

16: asSet.InsertCalcSet(Rp)

17: end

18: while algo=canCalculus() do

19: asSet.calculation(algo)

20: end

21: if algotype==2 then //迁移

22: asSet.InserttranSet(Cp)

23: while actlist!=NULL do

24: act=actlist.GetAction()

25: asSet.transition(act)

26: end

27: end

28: Input.Next()

29: end

30: return asSet。

算法中，1～4行分别声明了进程表达式、action数组、声明演算或迁移算法的引用和算法类型。6～10行分别从输入信息Input中获取API调用和事件序列、取得当前栈顶Activity所对应的进程表达式、取得IF-THEN规则名(算法引用)、获取算法类型(1为演算算法，2为迁移算法)。11～20行为演算操作，21～27行为迁移操作。其中calculation(calcRule)为进程演算算法，会依据指定的演算规则calcRule进行演算。transition(action)为进程迁移算法，由动作action驱动，依据迁移规则进行迁移，其迁移流程如图4所示。

图4 行为迁移流程Fig.4 Procedure of behavior transition

4.3 数据竞争检测

数据竞争检测的大体思路为：若操作共享数据的动作间包含了写操作，则对这些动作进行检测。动作间具有确定时序，则判定为正常；否则，判定为存在数据竞争问题。下面给出竞争关系集的数据结构。令raceRelationSet::={raceRelation}为竞争关系集，其中raceRelation为竞争关系，由竞争数据及其相关动作组成，即raceRelation::={racedata, {action}}。检测步骤如下。

(A)初始化竞争关系集。将目标App中的组件对象(如Activity对象、Service对象等)设置为竞争数据，并将与之有关的回调事件、UI事件、生命周期事件作为相关动作，构造竞争关系。

(B)扫描目标App的数据流图，利用文献[23]的方法获取共享数据和相关操作，加入raceRelationSet。

(C)在构造的raceRelationSet中，逐个检测竞争数据的使用是否遵循了条件护卫原则，若已遵循，则表明无数据竞争问题；若没有遵循，则转(D)。

(D)将与该共享数据相关的操作代入进程表达式，检测其时序关系，若其具有确定时序，表明无数据竞争问题；若没有，则表明存在数据竞争问题，生成检测报告。

其中，第(A)步是为了得到App环境(Android平台、UI操作等)中的数据竞争关系。下面以图1为例，说明具体的检测过程。

按照本文的建模方法，得到如下进程表达式。

PAsyncTask=υt1t2(PMainthread‖PBackgroundthread)

PAsyncApp=Paslifecycle‖PAsyncTask‖PonCreate。

PAsyncApp=Paslifecycle‖PAsyncTask‖PonCreate=

Paslifecycle‖υt1t2(PMainthread‖PBackgroundthread)‖PonCreate=

υt1t2(Paslifecycle‖PMainthread‖PBackgroundthread)‖PonCreate(SC-RES-COMP)=

从演算结果可以看出，onPostExecute和onDestroy之间没有交互通道，由安全约束2知，两者不存在时序约束，即其时序不确定，所以检测出数据竞争问题。

5 实验论证分析

5.1 实验环境

为了便于对比分析，采用文献[17]中提到的开源Apps验证本文方法的有效性，从精确性和效率两个方面进行评估，并与相关研究DroidRacer[17]、nAdroid[15]和Sard[16]进行对比。

建模过程需要使用Soot工具[24]进行控制流和数据流分析，资源消耗较高。因此，将建模与分析程序运行在Intel 3.20 GHz双核CPU，8 GiB内存的台式机上。操作系统为Linux (rhel-server-5.4)，使用eclipse-kepler-SR2进行编译和调试，Android的开发版本Android 6.0(API level 23)。测试用的开源Apps和运行时行为检测程序都运行在8 GiB RAM、128 GiB ROM的Honor V20，其处理器为Kirin 980。

运行时行为检测程序由API调用监测模块和检测模块组成。API调用监测模块采用API钩子(API hook)技术，得到运行中的Apps的API的触发时间、参数和返回值等信息。检测模块维护一个行为规则库，其中存储了IF-THEN格式的演算规则和迁移规则。依据行为规则，检测模块将API调用序列作为输入，驱动进程表达式进行演算和迁移，给出检测结果。

5.2 时空效率分析

a.c.τ(t).(b.0‖d.0)+c.a.τ(t).(b.0‖d.0)=

a.c.τ(t).b.d.0+a.c.τ(t).d.b.0+c.a.τ(t).b.d.0 +c.a.τ(t).d.b.0。

随着进程中有更多的动作数以及App中有更多的并发进程，行为迹的数目将呈指数级增长，求解或遍历程序的所有路径将会引起状态空间爆炸，导致极低的时空效率；不求解或遍历程序的所有路径，则会因检测覆盖面不全导致漏报问题。本文利用Pi演算的形式化和层次化特性，将各个子系统形式化为进程表达式，将子系统之间的时序、交互、同步和互斥等关系形式化为演算规则和迁移规则。依据这些规则，进程表达式通过并发演算可以还原出整个系统的结构信息。运行时行为检测过程中，本文所提模型由捕获的API驱动进行并发演算，这意味着，模型只会还原出程序该次运行所产生的路径和相关结构信息。若程序的某次运行，其路径上的API数为n，则模型的空间消耗为维护n个状态列表的开销，其规模与路径上的API数n呈线性增长关系。

为了体现出扩展Pi演算层次化的特点，本文的建模方法将并发的行为抽象成进程表达式的并发集合及其上的演算，形成封闭的代数空间。由于没有使用回溯算法，设进程表达式的长度为m，维护n个状态列表的情况下，本文方法总的时间开销为O(mn)，即运行时间是线性的，随着m规模的增大并不会显著地增加运行开销。

5.3 检测有效性分析

为了验证本文所提出方法的有效性并与相关研究DroidRacer、nAdroid和Sard对比，使用10款开源的测试程序进行数据竞争检测，结果如表1所示。其中检测结果列、误报数和漏报数列中由“/”分割的结果分别来自本文模型、DroidRacer、nAdroid和Sard。

从表1中可以看出，本文方法总计检出数据竞争81处，实际数据竞争为69处，误报15处，漏报3处。对比检测结果、误报数和漏报数可知，本文方法明显优于DroidRacer、nAdroid和Sard。这是因为本文方法通过将数据竞争的安全约束形式化地表示为包含进程表达式的IF-THEN规则，实现了行为模式和行为所需满足的安全策略之间的并发演算，这种机制可以非常容易地将现有的安全约束应用在该模型中。并且，本文采用的是动静态结合进行检测。本文将DroidRacer检测用户代码的读写竞争规则，nAdroid检测Android Apps中时序规则和Sard中对线程内和线程间并发错误的检测规则都以IF-THEN规则的形式纳入到本文模型中，因此有较高的精确性，且在提高检测精确性的同时并没有牺牲检测的效率。

表1 数据竞争检测结果

5.4 检测性能分析

选取表1中的Android Apps作为目标程序进行时空负载的测试并与DroidRacer、nAdroid和Sard进行对比分析，其时间负载和空间负载分别如图5、6所示。

由时间负载的测试结果可知，检测过程中，本文方法运行引起的正常CPU时间在5倍以下，其时间负载表现良好。DroidRacer和Sard引起的正常CPU时间在7倍以下，差强人意。nAdroid引起的正常CPU时间最高达到了9.5倍，明显高于其他方法，其检测精确性提高的同时检测效率却大大降低，这直接影响了其实用性。

从空间负载的测试结果来看，本文方法的内存空间增长率为3%～6%，非常稳定，空间负载表现出色。这是因为本文方法检测时并不需要将整个模型演算出来，而只需演算出待检测的部分进行状态迁移匹配，这有效地保障了模型的效率和实用性，测试结果也验证了这一点。其他3种方法受应用程序规模的影响较大，其中nAdroid的内存空间增长率为5%～12%，具有较高的空间负载。

图5 时间负载测试结果Fig.5 Result of time overhead

图6 空间负载测试结果Fig.6 Result of space overhead

6 结束语

本文针对事件驱动机制下的Android多线程程序的数据竞争问题，提出了一种形式化的行为检测模型。利用扩展后的Pi演算对Android生命周期和多线程框架进行建模，探讨了并发行为映射问题，并构建了并发行为的演算规则和迁移规则。扩展后的Pi演算的层次化特性适合于对Android Apps中组件化和基于通信的行为模式进行描述和检测。进程演算等形式化特性有助于实现行为建模和检测的自动化。通过将数据竞争的安全约束形式化地表示为包含进程表达式的IF-THEN规则，实现了行为模式和行为所需满足的安全策略之间的并发演算，构建了检测模型。将动态检测与静态检测以相同的处理方式结合在检测模型中，并给出了并发行为检测算法和数据竞争检测的方法。通过理论分析和实验验证，论证了该方法的检测有效性和检测性能。

本文模型特别适合对应用程序并发执行导致的数据竞争进行检测。演算规则越完备，模型越精确。但随着演算规则的规模越来越大，如何验证这些规则之间的一致性以规避规则的内在冲突，如何将相关的规则约简归并以进一步提高检测的效率是下一步亟需解决的问题。