PiCal2NuSMV为本文研究生阶段实现的一个从Pi-演算模型到SMV程序代码的自动转换工具。PiCal2lNuSMV共分为三大组件：Pi-演算文本解析器、转换适配器和SMV程序产生器。Pi-演算文本解析器用于把Pi-演算表达式的文本形式转化为内存表示形式，转换适配器基于此形式分析并转换Pi-演算进程为SMV程序的内存表示形式，SMV程序产生器将SMV程序内存表示方式转换为SMV程序代码文本。