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

作　　者：陈义[1] 唐郑熠[1] 

机构地区：[1]福建工程学院信息科学与工程学院,福建福州350118

出　　处：《福建电脑》2016年第3期39-40,50,共3页Journal of Fujian Computer

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

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

关 键 词：通信协议 ARQ协议 模型检测 SPIN PROMELA 

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