使用π-演算验证网络AB协议
AB协议就是窗口大小为1的滑动窗口协议,因而简单性和代表性而成为被广泛使用的范例.PiM是我们开发的一个π-演算的交互式验证工具.它也是第一个π-演算的交互式验证工具.PiM基于对多种互模拟关系的公理刻画,工作在语法层次上,可以交互式地验证两个进程是否是互模拟的.在本文中,我们使用π-演算对网络AB协议进行建模,并最终使用验证工具PiM证明了其正确性.在建模和证明过程中,我们还发现RobinMilner的著作Communication and Concurrency中有关AB协议的内容的一个可能的错误.
AB协议 验证工具 π-演算 互模拟 滑动窗口协议
杜旭涛 李舟军
国防科技大学计算机学院(湖南长沙)
国内会议
北京
中文
1119-1124
2003-11-01（万方平台首次上网日期，不代表论文的发表时间）