| 自动验证参数化Leader Election协议 |
| |
| 引用本文： | 徐蔚文,陆鑫达. 自动验证参数化Leader Election协议[J]. 计算机工程, 2003, 29(18): 14-15,153 |
| |
| 作者姓名： | 徐蔚文 陆鑫达 |
| |
| 作者单位： | 上海交通大学计算机科学与工程系,上海,200030 |
| |
| 基金项目： | 国家自然科学基金资助项目(60173103) |
| |
| 摘 要： | 讨论了一类Leader Election(LE)协议，该类协议通常运行在允许进程随时加入或崩溃的动态环境中，给出了LE协议的参数化版本，即考虑分布式系统中的进程数目任意多的情况。并提出了一种自动验证参数化LE协议的方法，用线性算数约束来模拟可能无限的全局状态集合，利用符号模型检测工具DMC[DP99]，文章实现了对参数化LE协议safety性质的自动验证。
|
| 关 键 词： | LE协议 参数化系统 形式验证 符号模型检测工具 |
| 文章编号： | 1000-3428(2003)18-0014-02 |
Automatic Verification of Parameterized Leader Election Protocols |
| |
| XU Weiwen,LU Xinda. Automatic Verification of Parameterized Leader Election Protocols[J]. Computer Engineering, 2003, 29(18): 14-15,153 |
| |
| Authors: | XU Weiwen LU Xinda |
| |
| 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. |
| |
| Keywords: | Leader Election protocol Parameterized system Formal verification |
| 本文献已被 CNKI 维普 万方数据 等数据库收录！ |
