随着计算机技术的迅速发展,计算机系统正变得愈加庞大和复杂,很多实际系统被赋予随机行为特征,我们需要使用模型检验的方法对随机系统进行自动的形式化验证,并定量分析其属性需求,这就是概率模型检验。概率模型检验是经典模型检验理论的推广和泛化,被广泛用于验证具有随机行为的计算机系统的定性和定量属性。在概率模型检验中分析的计算机系统包括自适应软件系统,这些系统在其生命周期内是动态变化的,为了在运行时验证这类系统,提出了运行时概率模型检验。运行时概率模型检验在很多方面的一个重要挑战是它的性能,它应该足够快地响应运行时需求,在运行时系统发生动态变化时持续验证当前系统是否满足系统要求。在本文中,针对运行时系统的概率模型检验效率问题,我们提出了一种针对运行时的增量概率模型检验方法,该方法用于随机模型在运行时的可达性概率计算中。本文提出的针对运行时的增量概率模型检验方法的主要特点是在运行时概率模型检验的验证过程中结合了两种启发式方法来提高其性能,这两种启发式方法通过在模型检验过程中再次使用模型发生变化前的可达性概率计算值和模型变化后对其状态重新排序来减少验证过程中的数值迭代次数,从而加速了数值迭代计算过程,提高了运行时概率模型检验效率。注意,本文的工作专注于提升在运行时发生某些变化的随机系统验证效率,我们的研究重点是对运行时系统的概率模型检验方法的改进,与运行时验证方法的选择无关。本文在模型检验工具PRISM中加入我们的启发式方法实现,并利用PRISM中的三类基准案例模型进行实验验证。实例研究中,我们使用了离散时间马尔可夫链(Discrete-Time Markov Chain,DTMC)来表示系统模型,使用概率时间树逻辑(Probabilistic Computation Tree Logic,PCTL)来规约需要验证的可达性属性。实验结果表明,在默认实验参数设置下本文所提出的针对运行时的增量概率模型检验可以将标准运行时概率模型检验的系统验证时间缩短至40%以上。本文的主要贡献如下:1对已有运行时概率模型检验的原理进行了剖析,针对运行时随机系统发生变化的情况,在运行时概率模型检验计算过程中结合两种启发式方法,提出了一种针对运行时的增量概率模型检验方法。2第一种启发式方法是增量值迭代。该启发式方法基于Gauss-Seidel迭代,初始DTMC模型概率值的计算结果被用作发生变化后的DTMC模型计算的初始值。3第二种启发式方法是模型变化后对状态重新排序。在数值迭代过程中根据模型的变化找到更好的状态排序来减少模型检验中数值计算的迭代次数。