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

Model checking of stop-and-wait ARQ via SPIN

作　　者：黄丽丽 HUANG Lili(School of Ecological Environment and Urban Construction,Fujian University of Technology,Fuzhou 350118,China)

机构地区：[1]福建工程学院生态环境与城市建设学院,福建福州350118

出　　处：《福建工程学院学报》2018年第3期253-258,共6页Journal of Fujian University of Technology

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

关 键 词：停等式ARQ SPIN PROMELA 模型检测 

分 类 号：TP393.08[自动化与计算机技术—计算机应用技术]