[1]黄丽丽.停等式ARQ协议的SPIN模型检测[J].福建工程学院学报,2018,16(03):253-258.[doi:10.3969/j.issn.1672-4348.2018.03.010]
　HUANG Lili.Model checking of stop-and-wait ARQ via SPIN[J].Journal of FuJian University of Technology,2018,16(03):253-258.[doi:10.3969/j.issn.1672-4348.2018.03.010]
点击复制

停等式ARQ协议的SPIN模型检测()
分享到：

《福建工程学院学报》[ISSN:2097-3853/CN:35-1351/Z]

卷:
第16卷
期数:
2018年03期
页码:
253-258
栏目:
出版日期:
2018-06-25

文章信息/Info

Title:
Model checking of stop-and-wait ARQ via SPIN
作者:
黄丽丽
福建工程学院生态环境与城市建设学院
Author(s):
HUANG Lili
School of Ecological Environment and Urban Construction, Fujian University of Technology
关键词:
停等式ARQ;  SPIN;  Promela;  模型检测
Keywords:
stop-and-wait ARQ;  SPIN;  Promela;  model checking
分类号:
TP393.08
DOI:
10.3969/j.issn.1672-4348.2018.03.010
文献标志码:
A
摘要:
介绍停等式ARQ协议的工作原理，并使用Promela对其进行建模，利用SPIN对所建模型进行检测，证明了所建模型具有停等式ARQ协议的性质。讨论对停等式ARQ协议进行攻击的方法，使用Promela语言对攻击者进行建模，并利用SPIN的图形界面工具XSPIN模拟了攻击过程，验证了攻击的有效性。
Abstract:
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.

参考文献/References:

[1] 李新宇.用于通信网络协议开发的形式化方法[J].中国新通信,2014(15):100-101.
[2] LU D L, CHANG J F. Performance of ARQ protocols in nonindependent channel errors[J]. IEEE Trans Commun, 1993, 41(5): 721-730.
[3] 徐佑军,谭敦茂,朱建武,等.蓝牙无线链路质量的分析、测试与改善[J].计算机工程与应用,2004,40(12):129-131，211.
[4] HOLZMANN G J. The model checker SPIN[J]. IEEE Transactions on Software Engineering,1997,23(5):279-295.
[5] 陈义,唐郑熠.通信协议的Promela语言建模与检测[J].福建电脑，2016,32(3):39-40.
[6] 徐永生.带参性质的形式化描述与证明[D].成都：电子科技大学,2015.
[7] 吴勇,李祥.基于TLA的ARQ协议描述与验证[J].计算机安全,2012(8): 40-43.

更新日期/Last Update: 2018-06-25