自动验证参数化Leader Election 协议

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

一种802.11eEDCA机制的优化算法

IEEE 802.11e增强型分布式信道访问机制对高优先级业务服务质量的保证,是通过牺牲低优先级业务服务质量来实现的。为避免这种信道资源分配不公平的现象,提出一种优化算法。将信道中部分时隙合并起来构成合并时隙,高优先级和低优先级业务在合并时隙中被先后发送,而单个时隙通常只发送低优先级业务。仿真结果表明,该算法可以提高业务的吞吐量,当站点数目增多时,高优先级业务和低优先级业务的吞吐量均表现稳定,可达到各种业务公平利用信道资源的目的。