近年来,越来越多的计算机科学方法被广泛应用到诸如生物学等领域。一方面,计算机科学的方法可以通过在计算机上进行模拟等方式使得对问题的研究可以摆脱原本复杂的实验环境和条件,大大节约了研究成本和研究时间,降低了研究难度;另一方面,计算机领域方法的多样性和计算机的强大计算能力,为复杂问题的解决提供了可能性。由于系统生物学和计算机科学研究中的复杂分布式系统有着类似的地方,形式化方法领域中的模型和验证技术可以被应用到系统生物学领域。形式化方法在分析大型系统方面优势明显,它有着高效的验证技术,可以利用自动化的计算机工具分析具有复杂行为的大型系统。作为一种表现良好的形式化方法,概率模型验证方法近年来广受人们的关注与研究。概率模型验证是从定量方面去检查一个具有随机性行为的有限状态系统的正确性。它与已有的基于仿真的方法有着一个明显的区别是它能对所要验证的系统进行彻底地挖掘,而不是仅仅挖掘系统的一个子集。本文将概率模型验证的方法应用到分析PDGF生物信号路径系统中。首先,作为本文的理论基础,本文详细讨论了概率模型验证的相关概念及理论推演。概率模型验证需要用到两种输入,即对系统的详细描述以及对系统属性的详细描述。本文首先给出了概率模型验证的含义以及对系统详细描述的方法,讨论了所要验证系统的瞬时概率和稳定概率的计算方法。接下来本文讨论了系统属性的描述方法,详细给出了文中用到的语言——CSL(持续概率逻辑),并对其扩展,即回报属性进行了讨论。另外,本文给出了关于文中所用的概率模型验证工具PRISM的详细介绍。其次,本文所要分析的PDGF生物信号路径系统对于细胞的繁殖和生长具有重要意义,它直接调控细胞分裂和增殖,与癌症的产生密切相关。本文详细分析了其组成,并将对其的研究细化为三个具体的目标,从而实现对PDGF生物信号路径的更好理解。再次,本文通过三组实验来实现了对三个目标的分析。实验中本文采用通过添加／移除单一反应来进行比较分析的方法,创建了多个模型的变种,以此来研究某一反应对路径信号的影响。这三组实验的结果显示,定量验证的方法能够帮助我们更加深刻的理解PDGF信号路径,更进一步地,能够提供一个关于路径行为的预测。最后,由于除了概率模型验证方法,许多基于仿真的方法在研究生物系统时也非常流行,本文选择了其中的常微分方程方法将其与概率模型验证方法进行了比较研究。对常微分方法的研究分为理论与实践两部分。理论方面,本文首先给出了常微分方程在生物系统中的概念,然后为了更好地与概率模型验证方法进行比较,本文详细讨论了常微分方法中瞬时状态行为与稳定状态行为的计算。在实践方面,本文给出了用常微分方法分析PDGF信号路径的详细实验过程,并将实验结果与概率模型验证方法的结果进行了比较分析。两种方法所的结果较为类似,本文进一步分析了两种方法类似与不同的原因。