通信协议的Promela语言建模与检测

作     者：陈义 唐郑熠 

作者机构：福建工程学院信息科学与工程学院福建福州350118 

基　　金：福建省中青年教师教育科研项目(JA15336 JB14069) 福建工程学院科研发展基金资助项目(GY-Z15087) 

出 版 物：《福建电脑》 (Journal of Fujian Computer)

年 卷 期：2016年第32卷第3期

页      码：39-40,50页

摘      要：通信协议的设计与分析是十分困难的工作。使用传统的方法已经难以保证协议设计的效率与质量,针对这一问题,提出了采用SPIN模型检测技术对通信协议进行分析的方法。以停等式ARQ协议为实例,抽象出它的模型并以Promela语言进行实现。同时,对协议的安全属性进行了分析,并转化为线性时序逻辑公式进行自动验证。最后,分析了停等式ARQ协议的缺陷,并在SPIN模型检测器中进行了验证。

主 题 词：通信协议 ARQ协议 模型检测 SPIN Promela 

学科分类：081203[081203] 08[工学] 0835[0835] 0812[工学-测绘类] 

D　O　I：10.16707/j.cnki.fjpc.2016.03.016

馆 藏 号：203124355...