随着网络技术的成熟,加速了各类网络设施、应用和服务的发展,如移动互联网、云计算等。它们渗透进了人们生活的方方面面。越来越多的设施与应用会建立在网络之上。研究如何保证它们的正确性和可靠性就变成一个有意义的课题。不同于其他软硬件系统,网络系统往往包含随机性。虽然业界目前主要采用测试来保证软硬件系统的正确性和可靠性。但是它也存在一些不足,如没有把握保证检测出系统所有的错误和其效果与测试者的经验有较大关联等。为更好地保证复杂随机系统的正确性和可靠性,我们提出了一种基于预测的贝叶斯统计模型检测方法(prediction-based Bayesian model checking)。从模型的初始状态开始,随机从模型中选择一条有限路径,并多次重复这个过程。由于有限路径是相互独立的,因此就能将所有的有限路径看作为样本,并通过贝叶斯推断(Bayesian Inference)来推断模型满足性质的概率。另外,我们利用贝叶斯统计学中先验分布与后验分布的共轭关系,在验证前预测所需样本的数量上限。并且保证一旦抽样数量达到该上限时,当前的结果已经达到了可信度与精度的要求,可立即返回。其次,根据之前所预测的上限,我们会在每次统计数据更新后,再次利用共轭关系来预测所有可能的推断结果。当所有可能的结果都与当前结果一致时,便直接返回结果。为提高对一部分复杂系统的验证效率(运行周期较长的随机系统),我们另外提出了一种启发式的抽样与验证算法。它将路径抽样与路径验证分开成两个阶段：在对路径进行验证时,尝试利用算法来定位一个“可判前缀”,而这个“可判前缀”能够直接用来判定该路径是否满足性质。而在后续的抽样中,根据之前所收集的“可判前缀”信息,便可以直接判断路径是否满足性质。从而避免耗时的路径验证。并且,它还可以与基于预测的贝叶斯统计模型检测算法相结合。SPAC(Statistical Probabilistic Approximate model Checker)是基于上述算法所实现的统计模型检测工具。通过SPAC对调度算法、分布式算法等案例进行研究后,发现在一些场景下,该算法相对于其他统计模型检测算法效率更高。并且对于运行周期较长的系统,启发式算法也可以进一步提高验证效率。