基于Pi演算的Android多线程程序的数据竞争检测
【摘要】 针对事件驱动机制下Android多线程程序的数据竞争问题，构造一个基于Pi演算的并发行为检测模型。利用扩展后的Pi演算对Android生命周期和多线程框架进行建模，得到形式化的行为模型；通过将安全约束抽象为形式化的IF-THEN规则，并利用Pi演算的性质进行进程演算和迁移，构建了检测模型；将动态检测与静态检测以相同的处理方式结合在检测模型中，并给出了并发行为检测算法和数据竞争检测的方法。理论分析和实验表明，本文所提出的方法具有线性的时间和空间复杂度，相比其他方法，在提高检测精确性的同时并没有牺牲检测的效率。
