小型微型计算机系统
小型微型計算機繫統
소형미형계산궤계통
MINI-MICRO SYSTEMS
2010年
8期
1484-1488
,共5页
杨晋吉%苏开乐%肖茵茵%李超明
楊晉吉%囌開樂%肖茵茵%李超明
양진길%소개악%초인인%리초명
有界模型检测%串空间%协议%验证%NuSMV
有界模型檢測%串空間%協議%驗證%NuSMV
유계모형검측%천공간%협의%험증%NuSMV
提出用BMC和串空间结合的方法对安全协议进行验证.首先是通过串空间的出测试理论先构造不安全协议的部分丛结构,通过该丛结构来约束协议运行的的规模和角色行为;然后用BMC对该丛结构进行建模,建立起对应的有限状态自动机和LTL验证规范,进行验证,有效减轻状态空间爆炸问题;利用不安全协议丛结构的特点,对BMC的下界进行优化.这种方式结合了模型检测和定理证明的优点,通过典型的安全协议的分析和实验,验证了本方法较传统的模型检测方法在验证安全协议时,验证效率提高明显.
提齣用BMC和串空間結閤的方法對安全協議進行驗證.首先是通過串空間的齣測試理論先構造不安全協議的部分叢結構,通過該叢結構來約束協議運行的的規模和角色行為;然後用BMC對該叢結構進行建模,建立起對應的有限狀態自動機和LTL驗證規範,進行驗證,有效減輕狀態空間爆炸問題;利用不安全協議叢結構的特點,對BMC的下界進行優化.這種方式結閤瞭模型檢測和定理證明的優點,通過典型的安全協議的分析和實驗,驗證瞭本方法較傳統的模型檢測方法在驗證安全協議時,驗證效率提高明顯.
제출용BMC화천공간결합적방법대안전협의진행험증.수선시통과천공간적출측시이론선구조불안전협의적부분총결구,통과해총결구래약속협의운행적적규모화각색행위;연후용BMC대해총결구진행건모,건립기대응적유한상태자동궤화LTL험증규범,진행험증,유효감경상태공간폭작문제;이용불안전협의총결구적특점,대BMC적하계진행우화.저충방식결합료모형검측화정리증명적우점,통과전형적안전협의적분석화실험,험증료본방법교전통적모형검측방법재험증안전협의시,험증효솔제고명현.
