计算机工程与科学
計算機工程與科學
계산궤공정여과학
COMPUTER ENGINEERING & SCIENCE
2006年
1期
12-15
,共4页
BRP%TLA+%ABP%规约%验证%模型检验
BRP%TLA+%ABP%規約%驗證%模型檢驗
BRP%TLA+%ABP%규약%험증%모형검험
BRP协议是为不可靠信道上传送大数据包文件设计的工业协议.该协议的正确性依赖于各部件实时方面的假设.本文主要阐述了使用时序规约语言TLA+对BRP协议进行规约和验证的过程.首先通过自然语言非形式化地描述BRP协议的基本原理和需求,在此基础上建立了BRP的形式化模型,利用TLA+先对不考虑实时要求的BRP进行规约,然后添加实时约束获得BRP完整的规约,最后使用模型检验器TLC验证BRP协议的各种性质.
BRP協議是為不可靠信道上傳送大數據包文件設計的工業協議.該協議的正確性依賴于各部件實時方麵的假設.本文主要闡述瞭使用時序規約語言TLA+對BRP協議進行規約和驗證的過程.首先通過自然語言非形式化地描述BRP協議的基本原理和需求,在此基礎上建立瞭BRP的形式化模型,利用TLA+先對不攷慮實時要求的BRP進行規約,然後添加實時約束穫得BRP完整的規約,最後使用模型檢驗器TLC驗證BRP協議的各種性質.
BRP협의시위불가고신도상전송대수거포문건설계적공업협의.해협의적정학성의뢰우각부건실시방면적가설.본문주요천술료사용시서규약어언TLA+대BRP협의진행규약화험증적과정.수선통과자연어언비형식화지묘술BRP협의적기본원리화수구,재차기출상건립료BRP적형식화모형,이용TLA+선대불고필실시요구적BRP진행규약,연후첨가실시약속획득BRP완정적규약,최후사용모형검험기TLC험증BRP협의적각충성질.
