摘要：P2P是构筑于互联网的大规模分布计算协议，采用形式化方法对P2P协议的本质原理进行分析，将有助于P2P协议的优化和改进。本文采用抽象状态机（ASM）对经典P2P协议Chord进行分析，用基于抽象状态机语言（Asml）对其建模，设计了核心运行规则，并得到了该协议的有限状态机模型。本文的工作有助于分析、优化P2P协议。

关键词：抽象状态机 chord协议 抽象状态机语言 有限状态机 

单位：国防科学技术大学计算机学院 湖南长沙410073