在智能时代,随着信息系统的规模和复杂度日益增大,人们对系统运行时的安全性和可靠性的要求越来越高。限界模型检测技术作为自动检验系统的有效手段,在提高系统可信性上发挥着重要作用。限界模型检测与插值序列相结合可以完成限定边界外属性的验证,进而实现无界模型检测。然而,插值序列的引入会增大模型编码的复杂程度,影响模型检测器整体的性能。针对这个问题,本文提出了基于插值的多核限界模型检测方法。本文的主要工作和创新点如下:首先,本文提出基于插值和状态空间划分的属性验证算法,将问题分解并利用多核技术并行求解。模型状态空间中的状态迁移路径被划分为路径簇,再利用限界模型检测和基于插值序列的可达性分析方法对路径簇进行验证。其次,利用路径簇中存在不动点的性质,本文提出路径簇剪枝算法,缩小待搜索状态空间的规模以提高检测效率。最后,为了进一步改进算法,本文提出了增量编码和验证假设两种优化方法。增量编码的思想是定量增加检测限界,减少约束求解器的调用次数。验证假设的思想是在模型检测中利用验证历史信息,将已验证过的属性加入到命题公式中,提高插值的求解效率。本文提出的基于插值的多核限界模型检测方法应用于层次状态变迁矩阵描述的系统模型的检验,验证了方法的正确性和有效性,相比于现有方法提高了检验结果的可信度。