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

Abstract:

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

Key words: PI-calculus, model checking, multicast, PIMSM protocol, inoculation, pruning