Skip to main content
Fachgebiete
Automobil + Motoren Bauwesen + Immobilien Business IT + Informatik Elektrotechnik + Elektronik Energie + Nachhaltigkeit Finance + Banking Management + Führung Marketing + Vertrieb Maschinenbau + Werkstoffe Versicherung + Risiko
DE
EN
Bücher
Zeitschriften
Themenseiten
Organisationspsychologie Projektmanagement Marketing Smart Manufacturing
Weitere Formate
Podcasts Webinare Technik Webinare Wirtschaft Kongresse Veranstaltungskalender Awards
Jetzt Einzelzugang starten
Zugang für Unternehmen
Referenzkunden
SLX-Digitalkonferenz: Zukunftswerkstatt 2024

Mehr Umsatz mit Top-Kontakten

Am 7. Mai erfahren Sie, wie Vertriebsteams Leadgenerierung, Leadnurturing und Leadstrategien effizient steuern können.
Erweiterte Suche
Anmelden
nach oben
Erschienen in:
Validation, Synthesis and Optimization for Cyber-Physical Systems Kapitel lesen Erstes Kapitel lesen

2017 | OriginalPaper | Buchkapitel

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

verfasst von : Ocan Sankur, Jean-Pierre Talpin

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

Verlag: Springer Berlin Heidelberg

Einloggen

Aktivieren Sie unsere intelligente Suche, um passende Fachinhalte oder Patente zu finden.

search-config
loading …

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.

Sie haben noch keine Lizenz? Dann Informieren Sie sich jetzt über unsere Produkte:

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!

Jetzt informieren

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!

Jetzt informieren

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!

Jetzt informieren
Vorheriges Kapitel Validation, Synthesis and Optimization for Cyber-Physical Systems
Nächstes Kapitel Combining String Abstract Domains for JavaScript Analysis: An Evaluation
Fußnoten
1
Both are denoted \(\alpha \). Formally, \(\alpha \) can be defined on the disjoint union of these sets.
 
2
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.
 
3
The source code and models are available at https://​github.​com/​osankur/​nusmv/​tree/​ftsp.
 
Literatur
1.
2.
Apt, K.R., Kozen, D.C.: Limits for automatic verification of finite-state concurrent systems. Inf. Process. Lett. 22(6), 307–309 (1986)MathSciNetCrossRef
3.
Baier, C., Katoen, J.-P.: Principles of Model Checking. MIT press, Cambridge (2008)MATH
4.
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
5.
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)
6.
Chang, E., Roberts, R.: An improved algorithm for decentralized extrema-finding in circular configurations of processes. Commun. ACM 22(5), 281–283 (1979)CrossRefMATH
7.
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
8.
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
9.
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)
Metadaten
Titel
An Abstraction Technique for Parameterized Model Checking of Leader Election Protocols: Application to FTSP
verfasst von
Ocan Sankur
Jean-Pierre Talpin
Copyright-Jahr
2017
Verlag
Springer Berlin Heidelberg
Buch
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-Jahr: 2017

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