本仓库为使用Trace运行态模型实现对Zookeeper集群中数据一致性、状态一致性以及其选举阶段、数据同步阶段、广播阶段
需要满足的属性进行形式化验证。
1.TraceVerification为规约验证需要的自定义TLC算子，规约代码
2.zookeeper-release-3.7.0为zookeeper插桩后的集群代码
3.论文链接:https://dl.acm.org/doi/10.1145/3558819.3558822
-
Notifications
You must be signed in to change notification settings - Fork 1
wirelesssecuritylab/ZookeeperTraceVerification
Folders and files
| Name | Name | Last commit message | Last commit date | |
|---|---|---|---|---|
Repository files navigation
About
本仓库为使用Trace运行态模型实现对Zookeeper集群中数据一致性、状态一致性以及其选举阶段、数据同步阶段、广播阶段 需要满足的属性进行形式化验证
Resources
Stars
Watchers
Forks
Releases
No releases published
Packages 0
No packages published