首页> 中文期刊>国防科技大学学报 >基于扩展标记变迁模型的时钟同步协议正确性验证

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

     

摘要

时钟同步协议是时间触发网络的一个重要组成部分,是时间触发网络实时性和确定性的关键.本文基于扩展标记变迁模型对时钟同步协议进行建模,基于模型检测方法对协议是否满足正确性属性进行验证.验证结果证明了在不同启动场景下时钟同步网络协议的正确性,也表明了扩展标记变迁模型对于协议验证的有效性.

著录项

  • 来源
    《国防科技大学学报》|2019年第3期|42-49|共8页
  • 作者单位

    中国航空无线电电子研究所,上海 200233;

    中国航空无线电电子研究所,上海 200233;

    清华大学 软件学院,北京 100084;

    北京信息科学与技术国家研究中心,北京 100084;

    信息系统安全教育部重点实验室,北京 100084;

    清华大学 软件学院,北京 100084;

    北京信息科学与技术国家研究中心,北京 100084;

    信息系统安全教育部重点实验室,北京 100084;

    清华大学 软件学院,北京 100084;

    北京信息科学与技术国家研究中心,北京 100084;

    信息系统安全教育部重点实验室,北京 100084;

  • 原文格式 PDF
  • 正文语种 chi
  • 中图分类 数字电路;
  • 关键词

    形式化方法; 协议验证; 模型检测;

  • 入库时间 2023-07-25 17:01:58

相似文献

  • 中文文献
  • 外文文献
  • 专利
获取原文

客服邮箱:kefu@zhangqiaokeyan.com

京公网安备:11010802029741号 ICP备案号:京ICP备15016152号-6 六维联合信息科技 (北京) 有限公司©版权所有
  • 客服微信

  • 服务号