【免费】基于扩展标记变迁模型的时钟同步协议正确性验证-发表之家

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

作者：曲国远; 徐晓飞; 刘威廷; 王沁煜; 贺飞中国航空无线电电子研究所; 上海200233; 清华大学软件学院; 北京100084; 北京信息科学与技术国家研究中心; 北京100084; 信息系统安全教育部重点实验室; 北京100084

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

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

注：因版权方要求，不能公开全文，如需全文，请咨询杂志社

学术咨询免费咨询杂志订阅

热门期刊服务

影响因子：0.6

期刊级别：北大期刊

发行周期：双月刊

服务介绍