自动验证参数化Leader Election协议

• 作者: 徐蔚文 陆鑫达
• 来源期刊: 计算机工程
• 学科: 工学
• 关键词: LE协议 参数化系统 形式验证
• 年，卷（期）: 2003,（18）
• 所属期刊栏目: 博士论文
• 页码范围: 14-15,153
• 页数: 3页
• 分类号: TP274+.5
• 字数: 3969字
• 语种: 中文
• DOI: 10.3969/j.issn.1000-3428.2003.18.006

摘要

讨论了一类Leader Election(LE)协议,该类协议通常运行在允许进程随时加入或崩溃的动态环境中,给出了LE协议的参数化版本,即考虑分布式系统中的进程数目任意多的情况.并提出了一种自动验证参数化LE协议的方法,用线性算数约束来模拟可能无限的全局状态集合,利用符号模型检测工具DMC[DP99],文章实现了对参数化LE协议safety性质的自动验证.

作者信息

序号	姓名	单位	发文数	被引次数	H指数	G指数
1	陆鑫达	上海交通大学计算机科学与工程系	60	406	9.0	18.0
2	徐蔚文	上海交通大学计算机科学与工程系	5	87	2.0	5.0