Top

Published in:

2017 | OriginalPaper | Chapter

An Abstraction Technique for Parameterized Model Checking of Leader Election Protocols: Application to FTSP

Authors : Ocan Sankur, Jean-Pierre Talpin

Published in: Tools and Algorithms for the Construction and Analysis of Systems

Publisher: Springer Berlin Heidelberg

Activate our intelligent search to find suitable subject content or patents.

search-config

AI-assisted search

Off

Abstract

We consider distributed timed systems that implement leader election protocols which are at the heart of clock synchronization protocols. We develop abstraction techniques for parameterized model checking of such protocols under arbitrary network topologies, where nodes have independently evolving clocks. We apply our technique for model checking the root election part of the flooding time synchronisation protocol (FTSP), and obtain improved results compared to previous work. We model check the protocol for all topologies in which the distance to the node to be elected leader is bounded by a given parameter.

Dont have a licence yet? Then find out more about our products and how to get one now:

Springer Professional "Wirtschaft+Technik"

Online-Abonnement

Mit Springer Professional "Wirtschaft+Technik" erhalten Sie Zugriff auf:

über 102.000 Bücher
über 537 Zeitschriften

aus folgenden Fachgebieten:

Automobil + Motoren
Bauwesen + Immobilien
Business IT + Informatik
Elektrotechnik + Elektronik
Energie + Nachhaltigkeit
Finance + Banking
Management + Führung
Marketing + Vertrieb
Maschinenbau + Werkstoffe
Versicherung + Risiko

Jetzt Wissensvorsprung sichern!

inform now

Springer Professional "Technik"

Online-Abonnement

Mit Springer Professional "Technik" erhalten Sie Zugriff auf:

über 67.000 Bücher
über 390 Zeitschriften

aus folgenden Fachgebieten:

Automobil + Motoren
Bauwesen + Immobilien
Business IT + Informatik
Elektrotechnik + Elektronik
Energie + Nachhaltigkeit
Maschinenbau + Werkstoffe

Jetzt Wissensvorsprung sichern!

inform now

Springer Professional "Wirtschaft"

Online-Abonnement

Mit Springer Professional "Wirtschaft" erhalten Sie Zugriff auf:

über 67.000 Bücher
über 340 Zeitschriften

aus folgenden Fachgebieten:

Bauwesen + Immobilien
Business IT + Informatik
Finance + Banking
Management + Führung
Marketing + Vertrieb
Versicherung + Risiko

Jetzt Wissensvorsprung sichern!

inform now

previous chapter Validation, Synthesis and Optimization for Cyber-Physical Systems

next chapter Combining String Abstract Domains for JavaScript Analysis: An Evaluation

Both are denoted \(\alpha \). Formally, \(\alpha \) can be defined on the disjoint union of these sets.

These labels can actually be defined within \(\varSigma (\mathsf{Id},\mathsf{Msg})\) by adding a special message content \(\texttt {tick}\) to \(\mathsf{Msg}\), and setting \(\texttt {tick}_i!=(n+1)!(i, \texttt {tick})\) where \(n+1\) is the identifier of \(\mathcal {S}\). We will write them simply as \(\texttt {tick}_i?\) and \(\texttt {tick}_i!\) to simplify the presentation.

The source code and models are available at https://github.com/osankur/nusmv/tree/ftsp.

Alur, R., Dill, D.L.: A theory of timed automata. Theoret. Comput. Sci. 126(2), 183–235 (1994)MathSciNetCrossRefMATH

Apt, K.R., Kozen, D.C.: Limits for automatic verification of finite-state concurrent systems. Inf. Process. Lett. 22(6), 307–309 (1986)MathSciNetCrossRef

Baier, C., Katoen, J.-P.: Principles of Model Checking. MIT press, Cambridge (2008)MATH

Bakhshi, R., Bonnet, F., Fokkink, W., Haverkort, B.: Formal analysis techniques for gossiping protocols. ACM SIGOPS Oper. Syst. Rev. 41(5), 28–36 (2007)CrossRef

Bingham, J.: Automatic non-interference lemmas for parameterized model checking. In: Proceedings of the 2008 International Conference on Formal Methods in Computer-Aided Design, FMCAD 2008, Piscataway, NJ, USA, pp. 11:1–11:8. IEEE Press (2008)

Chang, E., Roberts, R.: An improved algorithm for decentralized extrema-finding in circular configurations of processes. Commun. ACM 22(5), 281–283 (1979)CrossRefMATH

Chou, C.-T., Mannava, P.K., Park, S.: A simple method for parameterized verification of cache coherence protocols. In: Hu, A.J., Martin, A.K. (eds.) FMCAD 2004. LNCS, vol. 3312, pp. 382–398. Springer, Heidelberg (2004). doi:10.1007/978-3-540-30494-4_27 CrossRef

Clarke, E., Talupur, M., Veith, H.: Proving ptolemy right: the environment abstraction framework for model checking concurrent systems. In: Ramakrishnan, C.R., Rehof, J. (eds.) TACAS 2008. LNCS, vol. 4963, pp. 33–47. Springer, Heidelberg (2008). doi:10.1007/978-3-540-78800-3_4 CrossRef

Clarke, E.M., Grumberg, O., Long, D.E.: Model checking and abstraction. ACM Trans. Program. Lang. Syst. (TOPLAS) 16(5), 1512–1542 (1994)CrossRef

10.

Clarke Jr., E.M., Grumberg, O., Peled, D.A.: Model Checking. MIT Press, Cambridge (1999)

11.

Delzanno, G., Sangnier, A., Traverso, R.: Parameterized verification of broadcast networks of register automata. In: Abdulla, P.A., Potapov, I. (eds.) RP 2013. LNCS, vol. 8169, pp. 109–121. Springer, Heidelberg (2013). doi:10.1007/978-3-642-41036-9_11 CrossRef

12.

Desai, A., Seshia, S.A., Qadeer, S., Broman, D., Eidson, J.C.: Approximate synchrony: an abstraction for distributed almost-synchronous systems. In: Kroening, D., Păsăreanu, C.S. (eds.) CAV 2015. LNCS, vol. 9207, pp. 429–448. Springer, Cham (2015). doi:10.1007/978-3-319-21668-3_25 CrossRef

13.

Dolev, D., Klawe, M., Rodeh, M.: An o (n log n) unidirectional distributed algorithm for extrema finding in a circle. J. Algorithms 3(3), 245–260 (1982)MathSciNetCrossRefMATH

14.

Emerson, E.A., Namjoshi, K.S.: Reasoning about rings. In: Proceedings of the 22nd ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, POPL 1995, pp. 85–94. ACM, New York (1995)

15.

Garavel, H., Mounier, L.: Specification and verification of various distributed leader election algorithms for unidirectional ring networks. Sci. Comput. Program. 29(1), 171–197 (1997)CrossRef

16.

John, A., Konnov, I., Schmid, U., Veith, H., Widder, J.: Parameterized model checking of fault-tolerant distributed algorithms by abstraction. In: FMCAD, pp. 201–209 (2013)

17.

Fredlund, L., Groote, J.F., Korver, V.: Formal verification of a leader election protocol in process algebra. Theoret. Comput. Sci. 177(2), 459–486 (1997)MathSciNetCrossRefMATH

18.

Krstic, S.: Parameterized system verification with guard strengthening and parameter abstraction. In: Automated Verification of Infinite State Systems (2005)

19.

Kusy, B., Abdelwahed, S.: FTSP protocol verification using SPIN, May 2006

20.

Maróti, M., Kusy, B., Simon, G., Lédeczi, A.: The flooding time synchronization protocol. In: Proceedings of the 2nd International Conference on Embedded Networked Sensor Systems, SenSys 2004, pp. 39–49. ACM, New York (2004)

21.

McInnes, A.I.: Model-checking the flooding time synchronization protocol. In: IEEE International Conference on Control and Automation, ICCA 2009, pp. 422–429, December 2009

22.

McMillan, K.L.: Parameterized verification of the FLASH cache coherence protocol by compositional model checking. In: Margaria, T., Melham, T. (eds.) CHARME 2001. LNCS, vol. 2144, pp. 179–195. Springer, Heidelberg (2001). doi:10.1007/3-540-44798-9_17

23.

Milner, R.: A Calculus of Communicating Systems. Springer, New York (1982)MATH

24.

Pnueli, A.: The temporal logic of programs. In: 18th Annual Symposium on Foundations of Computer Science, pp. 46–57, October 1977

25.

Pnueli, A., Xu, J., Zuck, L.: Liveness with (0,1, \(\infty \))- counter abstraction. In: Brinksma, E., Larsen, K.G. (eds.) CAV 2002. LNCS, vol. 2404, pp. 107–122. Springer, Heidelberg (2002). doi:10.1007/3-540-45657-0_9 CrossRef

26.

Sugihara, R., Gupta, R.K.: Clock synchronization with deterministic accuracy guarantee. In: Marrón, P.J., Whitehouse, K. (eds.) EWSN 2011. LNCS, vol. 6567, pp. 130–146. Springer, Heidelberg (2011). doi:10.1007/978-3-642-19186-2_9 CrossRef

27.

Talupur, M., Tuttle, M.R.: Going with the flow: parameterized verification using message flows. In: Formal Methods in Computer-Aided Design, FMCAD 2008, pp. 1–8, November 2008

28.

Tan, L., Bu, L., Zhao, J., Wang, L.: Analyzing the robustness of FTSP with timed automata. In: Proceedings of the Second Asia-Pacific Symposium on Internetware, Internetware 2010, pp. 21:1–21:4. ACM, New York (2010)

29.

Vasudevan, S., Kurose, J., Towsley, D.: Design and analysis of a leader election algorithm for mobile ad hoc networks. In: Proceedings of the 12th IEEE International Conference on Network Protocols, ICNP 2004, pp. 350–360. IEEE (2004)

Title: An Abstraction Technique for Parameterized Model Checking of Leader Election Protocols: Application to FTSP
Authors: Ocan Sankur
Jean-Pierre Talpin
Publisher: Springer Berlin Heidelberg
Book: Tools and Algorithms for the Construction and Analysis of Systems
Print ISBN: 978-3-662-54576-8

Electronic ISBN: 978-3-662-54577-5

Copyright Year: 2017
DOI: https://doi.org/10.1007/978-3-662-54577-5_2

Springer Professional

Abstract

Please log in to get access to your license.

Dont have a licence yet? Then find out more about our products and how to get one now:

Springer Professional "Wirtschaft+Technik"

Springer Professional "Technik"

Springer Professional "Wirtschaft"

Premium Partner