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