概率模型检查在分析系统的可靠性、可用性等方面有非常重要的作用。在一些嵌入式控制系统或自适应系统中，运行环境是经常变化的。这些变化会导致模型的改变，也就需要我们频繁地进行模型检测。但是，因为参数变化过于频繁或者嵌入式系统受到运算能力或内存空间的限制，每当参数变化时都进行一次完整的模型检查是不能实现的。这时就需要高效的运行时模型检测方法。　　现有的带参数概率模型检测主要有两种方法。基于正规表达式转化的方法在实际运用中效率比较低，基于矩阵运算的方法中仅讨论了吸收马尔科夫链。这些方法都不适用于含有嵌套概率算子的公式。本文在现有研究的基础上，提出来基于强连通分支分解的带参数运行时模型检测方法，从而将原有的方法从吸收马尔科夫链拓展到了所有马尔科夫链。本文还给出了利用确定Rabin自动机对非嵌套PCTL*公式的带参数模型检查方法。对于含有嵌套概率算子的情况，在目的集合中任意两个状态都不属于同一个强连通分支的限制条件下，给出了对含有嵌套概率算子的可达性的验证方法。本文还根据以上的工作实现了一个实用的带参数运行时模型检测工具，利用该工具可以完成预处理阶段的模型检测以及运行时的求值。