计算机工程
計算機工程
계산궤공정
COMPUTER ENGINEERING
2003年
18期
14-15,153
,共3页
LE协议%参数化系统%形式验证
LE協議%參數化繫統%形式驗證
LE협의%삼수화계통%형식험증
讨论了一类Leader Election(LE)协议,该类协议通常运行在允许进程随时加入或崩溃的动态环境中,给出了LE协议的参数化版本,即考虑分布式系统中的进程数目任意多的情况.并提出了一种自动验证参数化LE协议的方法,用线性算数约束来模拟可能无限的全局状态集合,利用符号模型检测工具DMC[DP99],文章实现了对参数化LE协议safety性质的自动验证.
討論瞭一類Leader Election(LE)協議,該類協議通常運行在允許進程隨時加入或崩潰的動態環境中,給齣瞭LE協議的參數化版本,即攷慮分佈式繫統中的進程數目任意多的情況.併提齣瞭一種自動驗證參數化LE協議的方法,用線性算數約束來模擬可能無限的全跼狀態集閤,利用符號模型檢測工具DMC[DP99],文章實現瞭對參數化LE協議safety性質的自動驗證.
토론료일류Leader Election(LE)협의,해류협의통상운행재윤허진정수시가입혹붕궤적동태배경중,급출료LE협의적삼수화판본,즉고필분포식계통중적진정수목임의다적정황.병제출료일충자동험증삼수화LE협의적방법,용선성산수약속래모의가능무한적전국상태집합,이용부호모형검측공구DMC[DP99],문장실현료대삼수화LE협의safety성질적자동험증.
