基于扩展标记变迁模型的时钟同步协议正确性验证 |
| |
作者姓名: | 曲国远 徐晓飞 刘威廷 王沁煜 贺飞 |
| |
作者单位: | 中国航空无线电电子研究所,上海,200233;清华大学 软件学院,北京 100084;北京信息科学与技术国家研究中心,北京 100084;信息系统安全教育部重点实验室,北京 100084 |
| |
基金项目: | 航空科学基金资助项目(2015ZC15001);国家部委基金资助项目(3030603);国家自然科学基金资助项目(61672310,61272001,91218302) |
| |
摘 要: | 时钟同步协议是时间触发网络的一个重要组成部分,是时间触发网络实时性和确定性的关键。本文基于扩展标记变迁模型对时钟同步协议进行建模,基于模型检测方法对协议是否满足正确性属性进行验证。验证结果证明了在不同启动场景下时钟同步网络协议的正确性,也表明了扩展标记变迁模型对于协议验证的有效性。
|
关 键 词: | 形式化方法 协议验证 模型检测 |
收稿时间: | 2018-03-27 |
本文献已被 万方数据 等数据库收录! |
| 点击此处可从《国防科技大学学报》浏览原始摘要信息 |
|
点击此处可从《国防科技大学学报》下载免费的PDF全文 |
|