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

• 作者: 唐郑熠 陈义
• 来源期刊: 福建电脑
• 关键词: 通信协议 ARQ协议 模型检测 SPIN Promela
• 年，卷（期）: 2016,（3）
• 所属期刊栏目: 基金项目论文
• 页码范围: 39-40,50
• 页数: 3页
• 字数: 3093字
• 语种: 中文
• DOI: 10.16707/j.cnki.fjpc.2016.03.016

摘要

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

作者信息

序号	姓名	单位	发文数	被引次数	H指数	G指数
1	唐郑熠	福建工程学院信息科学与工程学院	17	19	3.0	3.0
2	陈义	福建工程学院信息科学与工程学院	3	2	1.0	1.0