本仓库为使用Trace运行态模型实现对Zookeeper集群中数据一致性、状态一致性以及其选举阶段、数据同步阶段、广播阶段
需要满足的属性进行形式化验证。
1.TraceVerification为规约验证需要的自定义TLC算子，规约代码
2.zookeeper-release-3.7.0为zookeeper插桩后的集群代码
3.论文链接:https://dl.acm.org/doi/10.1145/3558819.3558822
本仓库为使用Trace运行态模型实现对Zookeeper集群中数据一致性、状态一致性以及其选举阶段、数据同步阶段、广播阶段
需要满足的属性进行形式化验证。
1.TraceVerification为规约验证需要的自定义TLC算子，规约代码
2.zookeeper-release-3.7.0为zookeeper插桩后的集群代码
3.论文链接:https://dl.acm.org/doi/10.1145/3558819.3558822