中文摘要：

针对多线程并发程序生成覆盖同步语句的线程调度序列（TSS）效率低问题,提出了一种基于全同步对覆盖（APSC）准则的TSS生成（TGBA）方法。首先,对并发程序中的同步语句,定义了同步对及APSC;然后,给出了一个同步对-线程关联图（SPTG）构建方法;在此基础上,生成满足APSC的TSS;最后,使用JPF检测工具,对4个Java类库并发程序进行了TSS生成实验,并与常用的默认线程调度（DS）、抢占式线程调度（PS）和交叉线程调度（CS）序列生成方法在生成效率方面进行了对比分析。实验结果表明,与DS、CS方法相比,TGBA方法生成的TSS能够覆盖全部同步对;当满足APSC时,与PS方法相比,TGBA方法测试生成所需要的状态数、迁移数至少减少了19 889和44 352,并且生成效率平均提升了1.95倍,因此TGBA方法能够降低状态空间的规模开销,提高TSS的生成效率。

英文摘要：

Aiming at the problem of low efficiency on generating Thread Scheduling Sequence （TSS） that cover synchronization statements in multi-thread concurrent program, a TSS Generation Based on All synchronization pairs coverage criteria （TGBA） method was proposed. First, according to the synchronization statements in concurrent program, the synchronization pair and All Synchronization Pairs Coverage Criteria （APSE） were defined. Second, a construction method of Synchronization Pair Thread Graph （SPTG） was given. On that basis, TSSs that satisfied APSE were generated. Finally, by using JPF （Java PathFinder） detection tool, TSS generation experiments were conducted on four Java Library concurrent programs, and the comparison analysis of generation efficiency was conducted with general sequence generation methods of Default Scheduling （DS）, Preemptive Scheduling （PS） and Cross Scheduling （CS）. The experimental results illustrate that TSSs generated by TGBA method can cover all synchronization pairs compared to the DS and CS method. Moreover, when satisfying APSC, TGBA method decreases at least 19 889 states and 44 352 transitions compared to the PS method, and the average generation efficiency increases by 1.95 times. So TGBA method can reduce cost of state space and improve the efficiency of TSS generation.