多播协议PI演算建模与MWB检测  

PI-calculus Modeling of Multicast Protocol Verified with MWB

作　　者：张春永[1] 李祥[1] 

机构地区：[1]贵州大学计算机软件与理论研究所,贵州贵阳550025

出　　处：《计算机工程与科学》2008年第4期30-32,共3页Computer Engineering & Science

摘　　要：MWB是一个基于PI演算的模型检测工具。本文对多播的PIM_SM协议用PI演算建立一个三层模型并进行模型检测,其中主要检测PIM_SM协议中的嫁接和剪枝等;讨论利用PI演算建模的一般方法以及怎样利用MWB工具软件检测模型。MWB is a model checking tool based on PI-calculus. In this paper we make a three-layered model for the PIM SM protocol of multicast with PI-calculus and verify it, and mainly check the inoculation and pruning in the PIM-SM protocol. We also discuss the technique of PI-calculus modeling and how to use the MWB tool to check models.

关 键 词：PI演算 模型检测 多播 PIM_SM 协议 嫁接 剪枝 

分 类 号：TP393[自动化与计算机技术—计算机应用技术]