自动验证参数化Leader Election 协议

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

参数化系统二维抽象框架

针对参数化系统状态空间爆炸问题提出了一个通用的参数化系统二维抽象框架TDA。对所有进程单独进行抽象,利用参数化系统的设计思想,隐藏系统参数构建全系统的抽象模型,最大限度地剔除了原始系统中的冗余信息。建立的具有真并发语义的参数化系统的形式化模型,更适合描述一般意义上的并发系统,较好地解决了验证大规模同构和异构系统的空间激增问题。理论推导和实例均证实了TDA的正确性和合理性。

基于不变量查找的German协议验证

提出了一种通过查找缓存一致性协议不变量来验证带参协议正确性的新方法.缓存一致性协议验证的难点在于必须证明协议对于任意大小的带参系统都成立.我们通过寻找不变量和协议规则之间的对应关系来计算辅助不变量,从而帮助推导验证缓存一致性协议.我们设计实现了一个不变量查找工具并将该工具应用到German协议上计算它们的辅助不变量并成功地验证了协议的安全性质.

RCC高速缓存一致性协议的带参验证

Godson-T众核处理器的RCC高速缓存一致性协议是一种非常有特色的带参并发系统,对此协议的带参验证是一个很大的挑战.Cubicle是最近出现的基于SMT求解器的带参模型检测工具.我们使用了Cubicle带参模型检测工具,成功对RCC协议进行了建模和验证.实验结果表明,RCC协议在结点个数为任意规模时均满足协议的各种安全性质.

浅谈LoadRunner中Winsock参数化的实现

在使用性能测试工具LoadRunner测试socket协议的应用程序时，为了克服模拟测试时测试单一跟实际使用偏差较大，需要跟其他协议一样对测试脚本进行参数化，先在脚本中找到需要进行参数化的地方，再对其实行参数化，最终结果表明，在运行测试时，能够实现客户端向服务器端提交不同的数据，完成自动化性能测试。