摘要：MWB是一个基于PI演算的模型检测工具。本文对多播的PIM_SM协议用PI演算建立一个三层模型并进行模型检测，其中主要检测PIM_SM协议中的嫁接和剪枝等；讨论利用PI演算建模的一般方法以及怎样利用MWB工具软件检测模型。

关键词：pi演算 模型检测 多播 协议 嫁接 

单位：贵州大学计算机软件与理论研究所 贵州贵阳550025