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
Themenseiten
Organisationspsychologie Projektmanagement Marketing Smart Manufacturing
Bücher
Zeitschriften
Weitere Formate
Podcasts Webinare Technik Webinare Wirtschaft Kongresse Veranstaltungskalender Awards
Jetzt Einzelzugang starten
Zugang für Unternehmen
Referenzkunden
MTZ-Fachkongress

Antriebe und Energiesysteme von morgen


Austausch von Automobil- und Energiewirtschaft

Am 14./15. Mai geht es in Chemnitz um die Mobilitätswende durch Elektro- und Wasserstofffahrzeuge.
Erweiterte Suche
Anmelden
nach oben
Telecommunication Systems
Erschienen in: Telecommunication Systems 3/2015

01.03.2015

Modeling and analyzing the convergence property of the BGP routing protocol in SPIN

verfasst von: Zhe Chen, Daqiang Zhang, Yinxue Ma

Erschienen in: Telecommunication Systems | Ausgabe 3/2015

Einloggen

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

search-config
loading …

Abstract

The Border Gateway Protocol (BGP) is an interdomain routing protocol such that each autonomous system can independently formulate its routing policies. However, BGP does not always converge, because its routing policies may conflict and cause BGP to diverge, and result in persistent route oscillations. In this paper, we present an automated tool for verifying the convergence property of BGP by using the SPIN model checker. We have developed a SPIN library specifying a path vector protocol with a set of unspecified routing policies, and methods to instantiate the library to a specific BGP instance. The user only needs to provide models of network topology and customized routing policies, then SPIN can simulate the executions of the BGP instance, as well as automatically verify the protocol by exhaustively exploring all possible executions to detect possible divergences. The effectiveness of our library is demonstrated by experiments and verification results.
Vorheriger Artikel Tree-Code modeling and addressing for non-ID physical objects in the Internet of Things
Nächster Artikel Achieving an appropriate security level for distance bounding protocols over a noisy channel

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
Fußnoten
1
A state space is a directed graph where each possible state of a dynamical system is represented by a vertex, and there is a directed edge if and only if there is a state transition from one state to another. In words, the state space consists of all the states generated in verification. The state space explosion problem is the fact that the state space grows exponentially in the number of processes, resulting in an intractable size.
 
Literatur
1.
Abbas, C. J. B., González, R., Cardenas, N., & García-Villalba, L. J. (2008). A proposal of a wireless sensor network routing protocol. Telecommunication Systems, 38(1–2), 61–68.CrossRef
2.
Baier, C., & Katoen, J. P. (2008). Principles of model checking. Cambridge, MA: MIT Press.
3.
Ben-Ari, M. (2008). Principles of the SPIN model checker. Berlin: Springer.
4.
Chen, Y. S., Liao, Y. J., Lin, Y. W., & Chiu, G. M. (2009). Hve-mobicast: A hierarchical-variant-egg-based mobicast routing protocol for wireless sensornets. Telecommunication Systems, 41(2), 121–140.CrossRef
5.
Chen, Y. S., Lin, Y. W., & Pan, C. Y. (2011). Dir: Diagonal-intersection-based routing protocol for vehicular ad hoc networks. Telecommunication Systems, 46(4), 299–316.CrossRef
6.
Chen, Z., Motet, G. (2010). Nevertrace claims for model checking. In Proceedings of the 17th International SPIN Workshop on Model Checking of Software (SPIN 2010), Lecture Notes in Computer Science, (vol. 6349, pp. 162–179). Berlin: Springer.
7.
Clarke, E. M., Grumberg, O., & Peled, D. A. (2000). Model Checking. Cambridge, MA: MIT Press.
8.
Courcoubetis, C., Vardi, M. Y., Wolper, P., & Yannakakis, M. (1992). Memory-efficient algorithms for the verification of temporal properties. Formal Methods in System Design, 1(2/3), 275–288.CrossRef
9.
Gastin, P., Oddoux, D. (2001). Fast LTL to Büchi automata translation. In Proceedings of the 13th International Conference on Computer Aided Verification (CAV’01), Lecture Notes in Computer Science, (vol. 2102, pp. 53–65). Berlin: Springer.
10.
Gerth, R., Peled, D., Vardi, M. Y., & Wolper, P. (1995). Simple on-the-fly automatic verification of linear temporal logic. In P. Dembinski & M. Sredniawa (Eds.), Proceedings of the 15th IFIP WG6.1 International Symposium on Protocol Specification, Testing and Verification (pp. 3–18). London: Chapman & Hall.
11.
Griffin, T., Shepherd, F. B., & Wilfong, G. T. (2002). The stable paths problem and interdomain routing. IEEE/ACM Transactions on Networking (TON), 10(2), 232–243.CrossRef
12.
Griffin, T., & Wilfong, G.T. (1999). An analysis of bgp convergence properties. In Proceedings of the ACM SIGCOMM Conference on Applications, Technologies, Architectures, and Protocols for Computer Communication (SIGCOMM 1999), pp. 277–288.
13.
Herrmann, P., Krumm, H., Drögehorn, O., & Geisselhardt, W. (2002). Framework and tool support for formal verification of highspeed transfer protocol designs. Telecommunication Systems, 20(3–4), 291–310.CrossRef
14.
Holzmann, G. J. (1997). The model checker SPIN. IEEE Transactions on Software Engineering, 23(5), 279–295.CrossRef
15.
Holzmann, G. J. (1998). An analysis of bitstate hashing. Formal Methods in System Design, 13(3), 289–307.CrossRef
16.
Holzmann, G. J. (2003). The SPIN model checker: Primer and reference manual. Boston, MA: Addison-Wesley.
17.
Huadmai, C. (2011). Verification of routing policies by using model checking technique. In Proceedings of the IEEE 6th International Conference on Intelligent Data Acquisition and Advanced Computing Systems: Technology and Applications (IDAACS 2011), (vol. 2, pp. 711–716). IEEE.
18.
Huth, M., & Ryan, M. (2004). Logic in Computer science: Modelling and reasoning about systems (2nd ed.). Cambridge: Cambridge University Press.CrossRef
19.
Kettaf, N., Abouaissa, A., Duong, T. V., & Lorenz, P. (2006). An efficient QoS routing algorithm for solving MCP in ad hoc networks. Telecommunication Systems, 33(1–3), 255–267.CrossRef
20.
Myers, G. J. (1979). The art of software testing. Hoboken, NJ: Wiley.
21.
Rekhter, Y., & Li, T. (1995). A Border Gateway Protocol 4 (BGP-4), RFC 1771. IETF.
22.
Rekhter, Y., & Li, T. (2006). A Border Gateway Protocol 4 (BGP-4), RFC 4271. IETF.
23.
Secci, S., Rougier, J. L., Pattavina, A., Patrone, F., & Maier, G. (2011). Multi-exit discriminator game for BGP routing coordination. Telecommunication Systems, 48(1–2), 77–92.CrossRef
24.
Wang, A., Talcott, C. L., Jia, L., Loo, B. T., & Scedrov, A. (2011). Analyzing bgp instances in maude. In R. Bruni & J. Dingel (Eds.), Proceedings of the 31st IFIP WG 6.1 International Conference on Formal Techniques for Distributed Systems (FMOODS/FORTE 2011), Lecture Notes in Computer Science (vol. 6722, pp. 334–348). Berlin: Springer.
Metadaten
Titel
Modeling and analyzing the convergence property of the BGP routing protocol in SPIN
verfasst von
Zhe Chen
Daqiang Zhang
Yinxue Ma
Publikationsdatum
01.03.2015
Verlag
Springer US
Erschienen in
Telecommunication Systems / Ausgabe 3/2015
Print ISSN: 1018-4864
Elektronische ISSN: 1572-9451
DOI
https://doi.org/10.1007/s11235-014-9870-y

Weitere Artikel der Ausgabe 3/2015

Telecommunication Systems 3/2015 Zur Ausgabe

OriginalPaper

RFID-based mobility for seamless personal communication system in cloud computing

Original Paper

Tree-Code modeling and addressing for non-ID physical objects in the Internet of Things

Erratum

Erratum to: An RFID-based traceability system

OriginalPaper

Enabling RFID technology for healthcare: application, architecture, and challenges

OriginalPaper

Achieving an appropriate security level for distance bounding protocols over a noisy channel

OriginalPaper

Future RFID technology and applications: visions and challenges

Neuer Inhalt

    Bildnachweise