| 引用本文: | 曲国远,徐晓飞,刘威廷,等.基于扩展标记变迁模型的时钟同步协议正确性验证.[J].国防科技大学学报,2019,41(3):42-49.[点击复制] |
| QU Guoyuan,XU Xiaofei,LIU Weiting,et al.Correctness verification of clock synchronization protocol via extended labeled transition system models[J].Journal of National University of Defense Technology,2019,41(3):42-49[点击复制] |
|
| |
|
|
| 本文已被：浏览 6313次 下载 5234次 |
| 基于扩展标记变迁模型的时钟同步协议正确性验证 |
| 曲国远1, 徐晓飞1, 刘威廷2,3,4, 王沁煜2,3,4, 贺飞2,3,4 |
|
(1. 中国航空无线电电子研究所， 上海 200233;2.清华大学 软件学院， 北京 100084;3. 北京信息科学与技术国家研究中心， 北京 100084;4.信息系统安全教育部重点实验室， 北京 100084)
|
| 摘要: |
| 时钟同步协议是时间触发网络的一个重要组成部分，是时间触发网络实时性和确定性的关键。本文基于扩展标记变迁模型对时钟同步协议进行建模，基于模型检测方法对协议是否满足正确性属性进行验证。验证结果证明了在不同启动场景下时钟同步网络协议的正确性，也表明了扩展标记变迁模型对于协议验证的有效性。 |
| 关键词: 形式化方法 协议验证 模型检测 |
| DOI：10.11887/j.cn.201903008 |
| 投稿日期：2018-03-27 |
| 基金项目:航空科学基金资助项目（2015ZC15001）；国家部委基金资助项目（3030603）；国家自然科学基金资助项目（61672310,61272001,91218302） |
|
| Correctness verification of clock synchronization protocol via extended labeled transition system models |
| QU Guoyuan1, XU Xiaofei1, LIU Weiting2,3,4, WANG Qinyu2,3,4, HE Fei2,3,4 |
|
(1. China Aeronautical Radio Electronics Research Institute, Shanghai 200233, China;2.School of Software, Tsinghua University, Beijing 100084, China;3.Beijing National Research Center for Information Science and Technology, Beijing 100084, China;4.Key Laboratory for Information System Security, Ministry of Education, Beijing 100084, China)
|
| Abstract: |
| Clock synchronization protocol, as an important component of the time-triggered networks, is the key to the instantaneity and certainty of the time-triggered networks. The modeling and verification of clock synchronization protocol were studied. The protocol′s behaviors were modeled by the extended labeled transition systems, and its correctness was verified by model checking technique. The verification results certified the correctness of this protocol even under different startup scenarios. Experimental results also show the effectiveness of extended labeled transition systems in protocol verification. |
| Keywords: formal methods protocol verification model checking |
|
|
|
|
|
