Petri网已经被广泛的应用在模拟和分析并发与分布式系统上。并发与分布式系统的开发中 Petri 网的验证和确认是非常重要的。除了形式分析技术以外，已经证明测试在检测系统错误方面的有效性，并且它易于应用。系统的、有效的测试 Petri 网的方法之一是建立一个测试标准，使得测试充分性可以客观的被度量。 本文主要测试一种高级Petri 网—谓词/变迁网(Pr/T网)，Pr/T 网适合定义基本并发系统的控制、数据、功能和动态行为。文中首先对 Petri 网和测试知识进行了概述；在高级 Petri 网方面，主要探讨了谓词/变迁网的语法和静态语义、动态语义以及测试过程中可观察的行为；接着阐述了面向状态的测试方法和面向变迁的测试方法；其次研究了观察和记录测试结果的方法，给出了度量测试充分性的测试标准集；然后在说明建立Pr/T网模型方法的基础上，对哲学家就餐问题建立了Pr/T网模型，并应用面向状态的测试方法和面向变迁的测试方法测试了Pr/T网；文中引入了一种模型检查验证的工具—SPIN，它使用PROMELA作为它的规格说明语言；文中把哲学家就餐问题的Pr/T网转换成Promela程序，通过在Cygwin系统虚拟 Linux 环境下，启动 Xspin，运行哲学家就餐问题Pr/T网的Promela程序，模拟实验表明哲学家就餐问题的Pr/T网中所有的变迁和状态都被充分的覆盖到。