基于扩展标记变迁模型的时钟同步协议正确性验证
|
摘要
时钟同步协议是时间触发网络的一个重要组成部分,是时间触发网络实时性和确定性的关键。本文基于扩展标记变迁模型对时钟同步协议进行建模,基于模型检测方法对协议是否满足正确性属性进行验证。验证结果证明了在不同启动场景下时钟同步网络协议的正确性,也表明了扩展标记变迁模型对于协议验证的有效性。
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.
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.
引文
[1]Time-triggered Ethernet:SAE AS6802[S]. SAE International,2011.
[2]Steiner W. TTEthernet specification[R]. TTA Group,2008.
[3]Kopetz H,Ademaj A,Grillinger P,et al. The time-triggered Ethernet(TTE)design[C]//Proceedings of 8th IEEE International Symposium on Object-oriented Real-time Distributed Computing,2005.
[4]He F,Yin L Z,Wang D X,et al. Beagle user manual[R].Beijing:Tsinghua University,2013.
[5]Clarke E M,Grumberg O,Peled D A. Model checking[M].UK:MIT Press,1999.
[6]Mc Millan K L. Symbolic model checking[M]. USA:Springer US,1993:25-60.
[7]He F,Yin L Z,Wang B Y,et al. VCS:a verifier for component-based systems[C]//Proceedings of 11th International Symposium on Automated Technology for Verification and Analysis,2013:478-481.
[8]Yin L Z,He F,Gu M,et al. Clause replication and reuse in incremental temporal induction[C]//Proceedings of International Conference on Engineering of Complex Computer Systems,2014.
[9]Yin L Z,He F,Gu M. Reusing search tree for incremental SAT solving of bounded model checking[C]//Proceedings of International Conference on Engineering of Complex Computer Systems,2013:85-92.
[10]Yin L Z,He F,Gu M. Optimizing the SAT decision ordering of bounded model checking by structural information[C]//Proceedings of 7th International Symposium on Theoretical Aspects of Software Engineering,2013:23-26.
[11]Roy A, Gopinath K. Improved probabilistic models for802. 11 protocol verification[C]//Proceedings of International Conference on Computer Aided Verification, 2005:239-252.
[12]Esparza J, Ganty P, Leroux J, et al. Verification of population protocols[J]. Acta Informatica, 2017, 54:191-215.
[13]He F,Baresi L,Ghezzi C,et al. Formal analysis of publishsubscribe systems by probabilistic timed automata[C]//Proceedings of 27th IFIP WG 6. 1 International Conference on Formal Methods for Networked and Distributed Systems,2007:247-262.
[14]Steiner W,Dutertre B. SMT-based formal verification of a TTEthernet synchronization function[C]//Proceedings of 15th Workshop on Formal Methods for Industrial Critical Systems,2010:148-163.
[15]Steiner W,Dutertre B. Automated formal verification of the TTEthernet synchronization quality[C]//Proceedings of NASA Formal Methods Symposium,2011:375-390.
[16]Steiner W, Dutertre B. The TTEthernet synchronization protocols and their formal verification[J]. International Journal of Critical Computer-Based Systems,2013,4(3):280-300.
[2]Steiner W. TTEthernet specification[R]. TTA Group,2008.
[3]Kopetz H,Ademaj A,Grillinger P,et al. The time-triggered Ethernet(TTE)design[C]//Proceedings of 8th IEEE International Symposium on Object-oriented Real-time Distributed Computing,2005.
[4]He F,Yin L Z,Wang D X,et al. Beagle user manual[R].Beijing:Tsinghua University,2013.
[5]Clarke E M,Grumberg O,Peled D A. Model checking[M].UK:MIT Press,1999.
[6]Mc Millan K L. Symbolic model checking[M]. USA:Springer US,1993:25-60.
[7]He F,Yin L Z,Wang B Y,et al. VCS:a verifier for component-based systems[C]//Proceedings of 11th International Symposium on Automated Technology for Verification and Analysis,2013:478-481.
[8]Yin L Z,He F,Gu M,et al. Clause replication and reuse in incremental temporal induction[C]//Proceedings of International Conference on Engineering of Complex Computer Systems,2014.
[9]Yin L Z,He F,Gu M. Reusing search tree for incremental SAT solving of bounded model checking[C]//Proceedings of International Conference on Engineering of Complex Computer Systems,2013:85-92.
[10]Yin L Z,He F,Gu M. Optimizing the SAT decision ordering of bounded model checking by structural information[C]//Proceedings of 7th International Symposium on Theoretical Aspects of Software Engineering,2013:23-26.
[11]Roy A, Gopinath K. Improved probabilistic models for802. 11 protocol verification[C]//Proceedings of International Conference on Computer Aided Verification, 2005:239-252.
[12]Esparza J, Ganty P, Leroux J, et al. Verification of population protocols[J]. Acta Informatica, 2017, 54:191-215.
[13]He F,Baresi L,Ghezzi C,et al. Formal analysis of publishsubscribe systems by probabilistic timed automata[C]//Proceedings of 27th IFIP WG 6. 1 International Conference on Formal Methods for Networked and Distributed Systems,2007:247-262.
[14]Steiner W,Dutertre B. SMT-based formal verification of a TTEthernet synchronization function[C]//Proceedings of 15th Workshop on Formal Methods for Industrial Critical Systems,2010:148-163.
[15]Steiner W,Dutertre B. Automated formal verification of the TTEthernet synchronization quality[C]//Proceedings of NASA Formal Methods Symposium,2011:375-390.
[16]Steiner W, Dutertre B. The TTEthernet synchronization protocols and their formal verification[J]. International Journal of Critical Computer-Based Systems,2013,4(3):280-300.