《表1 实验结果：基于扩展标记变迁模型的时钟同步协议正确性验证》

  提示：宽带有限、当前游客访问压缩模式

本系列图表出处文件名：随高清版一同展现

《基于扩展标记变迁模型的时钟同步协议正确性验证》

1. 获取 高清版本忘记账户？点击这里登录

1. 下载图表忘记账户？点击这里登录

验证结果如表1所示，其中第1列表示验证的属性，第2列和第3列表示网络中包含的CM和SM数量，第4列为启动模式（第2节中介绍的3种启动模式分别以1，2，3表示）。采用限界模型检测执行验证，第5列表示限界模型检测展开的步数，第6列表示验证所需的时间，第7列表示属性验证的结果。注意属性P1为true、属性P2为false为期望的模型验证结果。