停等式ARQ协议的SPIN模型检测

介绍停等式ARQ协议的工作原理，并使用Promela对其进行建模，利用SPIN对所建模型进行检测，证明了所建模型具有停等式ARQ协议的性质。讨论对停等式ARQ协议进行攻击的方法，使用Promela语言对攻击者进行建模，并利用SPIN的图形界面工具XSPIN模拟了攻击过程，验证了攻击的有效性。

Model checking of stop-and-wait ARQ via SPIN

The working principle of the stop-and-wait ARQ was introduced, whose model was established by using the Promela language. The established model was proved, through model testing conducted with SPIN, to have the nature of the stop-and-wait ARQ. Then the method of attacking the ARQ protocol was discussed, and the attacker was modeled by using the Promela language. The attack process was simulated by using SPIN’s graphical interface tool XSPIN, which proved the effectiveness of the attack.