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

关键词: LE协议, 参数化系统, 形式验证

Abstract: The well-known problem of Leader Election is considered in a dynamic context which processes may participate or crash spontaneously, and processes communicate by means of buffered broadcasting. This paper considers a class of Leader Election protocols designed for such dynamic system, and proposes a new method for the verification of parameterized Leader Election protocols.This approach uses linear arithmetic constraints to model possibly infinite sets of global states. Using symbolic model checker DMC [DP99], it automatically verifies safety properties for parameterized Leader Election protocols.

中图分类号: 

• TP393