基于Pi演算的Android多线程程序的数据竞争检测

王涛; 马川

doi:10.16088/j.issn.1001-6600.2020.02.004

广西师范大学学报（自然科学版） ›› 2020, Vol. 38 ›› Issue (02) : 29 -42. DOI: 10.16088/j.issn.1001-6600.2020.02.004

基于Pi演算的Android多线程程序的数据竞争检测

王涛, 马川

作者信息 +

Author information +

文章历史 +

PDF

摘要

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