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