循环作为代码的基本结构,在程序执行过程中可能有不终止的现象发生。在系统运行过程中由循环的不终止造成的漏洞往往难以发现,并且该漏洞如果被攻击者利用将会对系统造成拒绝服务器攻击。因此,在软件开发过程中,对循环的终止性检测对保证软件的质量有着重要的意义。本文基于路径依赖自动机理论提出了多路径线性循环终止性分析方法。首先,利用路径依赖自动机理论对多路径线性循环进行建模,在建模过程中利用线性循环终止性理论分析模型中每条可迭代路径的终止性,并针对线性循环构成的路径提出了利用最弱后置条件确定两路径之间依赖关系的算法。在完成循环建模后,本文扩展了线性循环终止性理论使其支持带有前置条件的循环的终止性的判定,并根据路径之间的依赖关系构造路径的前置条件,对在建模过程中给出‘终止性未知’的路径进行终止性分析。最后,提出了路径依赖自动机中环结构终止性的分析方法,以确定路径之间交替执行对终止性的影响,并根据各路径自身的终止性与环结构的终止性确定循环整体的终止性。依据上述方法,本文实现了循环终止性分析工具Loopster++。本文通过分析程序验证比赛中测试样例的终止性并通过与其他优秀的工具进行对比实验证明了Loopster++的有效性和高效性。实验结果表明,Loopster++在对多路径线性循环的终止性分析上是有效的,并且在求解效率上要比其他工具快至少5倍。