模型检验是一种自动且完备的形式化验证方法。对于有限状态系统和时序逻辑公式,模型检验可以判定给定的系统模型是否满足公式中对性质或规范的逻辑描述,以此来验证系统模型是否满足性质规约,并可以在系统模型不满足性质规约时提供反例。随机模型检验是经典模型检验理论的推广和泛化,可对随机系统进行基于模型的定量验证。由于结合了经典模型检验算法和计算概率的数值方法,随机模型检验面临着更为严重的状态爆炸问题(state explosion problem)。因此如何缓解随机模型检验过程中的状态爆炸问题,是随机模型检验应用的关键性挑战问题。论文的贡献及成果主要体现在下述几个方面:(1)首次将对称假设-保证规则(symmetric assume-guarantee rule,SYM)应用到两组件随机系统的模型检验中,同时基于NL*学习算法为概率自动机(Probabilistic automata,PA)的组合随机模型检验提出了一种SYM-NL框架。(2)对现有的组合随机模型检验过程进行了优化,使其在系统模型不满足概率安全性质的情况下,能够更快的得到验证结果,从而避免一些因错误而产生的不必要的损失。(3)将SYM规则扩展为可用于检验多组件系统的SYM-n规则,并扩展上述的框架使其支持SYM-n规则。实际上,在本文的假设-保证式组合随机模型检验(assume-guarantee compositional stochastic model checking,AG-CSMC)方法中,假设的产生过程是一个迭代的学习过程,我们的优化是通过减少学习过程的迭代次数,从而提高算法的运行效率。在PRISM的基础上,我们设计了一个原型工具来实际验证几个大规模实例,包括传感器网络模型、客户-服务器模型和随机一致性算法模型。实验的目的分为三个方面:(1)验证论文的方法是否可行;(2)验证论文对检验过程的优化是否有效;(3)验证SYM-n规则是否比SYM规则更有优势。实验结果表明,我们的原型工具可以成功检验所有的实例,并且与现有的方法相比,我们的原型工具在模型不满足性质的情况下,检验所需时间更少。此外,通过SYM规则与SYM-n规则的对比实验,我们发现对于大规模实例,SYM-n规则明显优于SYM规则。