针对谓词/变迁网缺乏有效的形式化验证分析技术,基于代数规约测试谓词/变迁网方法,给出谓词/变迁网转换成代数规约语言CASOCC-WS表示的基调的规则,提出基于测试充分性准则深度优先遍历谓词/变迁网生成变迁触发序列的算法和由变迁触发序列构造公理等式的启发式规则.案例研究表明:该方法可以有效地解决测试Pr/T网时自动生成测试用例和自动判定测试结果和可行路径的问题. In the absence of an effective formal verification analysis technique for predicate / transition network, the rules of predicate / transition net transformation from predicate / transition network to CASOCC-WS representations are given based on the algebraic protocol test predicate / transition net method. The test adequacy criterion Depth-first traversal of predicate / transition network to generate transition trigger sequence and heuristic rule of constructing axiom equation from transition trigger sequence.The case study shows that this method can effectively solve the problem of automatically generating test cases and automatically judging when testing Pr / T network Test results and feasible path problems.