计算机应用
計算機應用
계산궤응용
COMPUTER APPLICATION
2013年
z2期
235-237,268
,共4页
Promela%SPIN%协议验证%载波监听多路访问/冲突检测机制%形式化
Promela%SPIN%協議驗證%載波鑑聽多路訪問/遲突檢測機製%形式化
Promela%SPIN%협의험증%재파감은다로방문/충돌검측궤제%형식화
Promela%SPIN (Simple Promela INtepreter)%protocol validation%Carrier sense Multiple Access with Collision Detection (CSMA/CD)%formalization
模型检测是协议验证的技术之一.在CSMA/CD协议的验证过程中对该协议进行了简化,忽略了通道时延、退避算法等细节,运用Promela语言进行建模实现.最后,使用模型检测工具SPIN对协议实现的正确性、状态可达性以及可能存在的不可推进循环进行了分析和检验,并从结果的有效性和正确性方面得出了相应验证输出图.
模型檢測是協議驗證的技術之一.在CSMA/CD協議的驗證過程中對該協議進行瞭簡化,忽略瞭通道時延、退避算法等細節,運用Promela語言進行建模實現.最後,使用模型檢測工具SPIN對協議實現的正確性、狀態可達性以及可能存在的不可推進循環進行瞭分析和檢驗,併從結果的有效性和正確性方麵得齣瞭相應驗證輸齣圖.
모형검측시협의험증적기술지일.재CSMA/CD협의적험증과정중대해협의진행료간화,홀략료통도시연、퇴피산법등세절,운용Promela어언진행건모실현.최후,사용모형검측공구SPIN대협의실현적정학성、상태가체성이급가능존재적불가추진순배진행료분석화검험,병종결과적유효성화정학성방면득출료상응험증수출도.
