论文部分内容阅读
在很多领域中都有带参系统的实际应用，如缓存一致性协议、安全系统和网络通信协议等。一般而言，带参系统中存在多个完全相同的并发进程，这些进程的个数即带参系统的参数。对带参系统进行形式化验证是一个颇具挑战性的困难问题，因为需要证明其安全性质在任意参数下都能够成立。针对这一问题，本文进行了以下方面的工作: 1.设计了调用第三方工具的客户端/服务器架构，以达到提高查询效率、分解大型任务、实现结果复用等目的; 2.提出了一个形式化语义模型并构建了相关工具，设计并实现了验证工具ParaVerifer，应用一系列启发式策略来自动生成因果关系和辅助不变式，并最终生成Isabelle证明脚本; 3.能够进行简单的流图分析，对一些带参系统状态的典型迁移过程给出直观的表示，有助于加深对带参系统的理解。 ParaVerifer验证工具能够完成对MESI、German和Flash等一系列基准测试用例的完整形式验证工作，且能够对这些带参系统中的典型状态迁移流进行分析并给出直观的图形表示。