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:
XSpeed: Accelerating Reachability Analysis on Multi-core Processors Kapitel lesen Erstes Kapitel lesen

2015 | OriginalPaper | Buchkapitel

Limited Mobility, Eventual Stability

verfasst von : Lenore D. Zuck, Sanjiva Prasad

Erschienen in: Hardware and Software: Verification and Testing

Verlag: Springer International Publishing

Einloggen

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

search-config
loading …

Abstract

The IPv6 Mobility protocol, an archetypal system for supporting communication amongst mobile devices, presents challenging verification problems. While model-checking techniques have been used to illustrate subtle oversights and flaws in the informal specifications previously, the more difficult question — whether it is possible to verify the correctness of the core architecture by checking properties on a small model — has not been adequately examined. In this paper we present a novel technique combining ideas from verification of parameterised systems, abstraction, model-checking of temporal logic properties and simulation relations found in process algebras. The technique relies on the fact that the system can be considered to eventually stabilise to a form more amenable to techniques used for model-checking parameterised systems, allowing the checking of arbitrary LTL properties.

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 Parallel Symbolic Execution: Merging In-Flight Requests
Nächstes Kapitel A New Refinement Strategy for CEGAR-Based Industrial Model Checking
Fußnoten
1
IP only promises a best effort at datagram delivery; there are the usual reasons for non-delivery of messages: node failure, link failure, noisy traffic, inadequate buffer space at congested nodes, etc. The question thus is whether mobility adduces any additional reasons for non-deliverability of messages.
 
2
In fact, some of the published works incorrectly claim that messages do not traverse cycles.
 
Literatur
1.
Amadio, R.M., Prasad, S.: Modelling IP mobility. Formal Methods Syst. Design 17(1), 61–99 (2000)CrossRef
2.
Arons, T., Pnueli, A., Ruah, S., Xu, J., Zuck, L.D.: Parameterized verification with automatically computed inductive assertions. In: Berry, G., Comon, H., Finkel, A. (eds.) CAV 2001. LNCS, vol. 2102, p. 221. Springer, Heidelberg (2001) CrossRef
3.
Balaban, I., Pnueli, A., Sa’ar, Y., Zuck, L.D.: Verification of multi-linked heaps. J. Comput. Syst. Sci. 78(3), 853–876 (2012)MathSciNetCrossRefMATH
4.
Balaban, I., Pnueli, A., Zuck, L.D.: Invisible safety of distributed protocols. In: Bugliesi, M., Preneel, B., Sassone, V., Wegener, I. (eds.) ICALP 2006. LNCS, vol. 4052, pp. 528–539. Springer, Heidelberg (2006) CrossRef
5.
Balaban, I., Pnueli, A., Zuck, L.D.: Shape analysis of single-parent heaps. In: Cook, B., Podelski, A. (eds.) VMCAI 2007. LNCS, vol. 4349, pp. 91–105. Springer, Heidelberg (2007) CrossRef
6.
Dang, Z., Kemmerer, R.A.: Using the ASTRAL model checker to analyze mobile IP. In: Proceedings of the 1999 International Conference on Software Engineering, ICSE 1999, Los Angeles, 16–22 May 1999, pp. 132–142 (1999)
7.
Emerson, E.A., Kahlon, V.: Reducing model checking of the many to the few. In: Proceedings Automated Deduction - CADE-17, 17th International Conference on Automated Deduction, Pittsburgh, 17–20 June 2000, pp. 236–254 (2000)
8.
Fang, Y., McMillan, K.L., Pnueli, A., Zuck, L.D.: Liveness by invisible invariants. In: Najm, E., Pradat-Peyre, J.-F., Donzeau-Gouge, V.V. (eds.) FORTE 2006. LNCS, vol. 4229, pp. 356–371. Springer, Heidelberg (2006) CrossRef
9.
Fang, Y., Piterman, N., Pnueli, A., Zuck, L.D.: Liveness with invisible ranking. STTT 8(3), 261–279 (2006)CrossRefMATH
10.
11.
Jackson, D., Ng, Y.-C., Wing, J.M.: A nitpick analysis of mobile IPv6. Formal Aspects Comput. 11(6), 591–615 (1999)CrossRefMATH
12.
13.
McCann, P.J., Roman, G.-C.: Modeling mobile IP in mobile unity. ACM Trans. Softw. Eng. Methodol. 8(2), 115–146 (1999)CrossRef
14.
Perkins, C., Johnson, D., Arkko, J.: Mobility Support in IPv6. RFC 6275 (Proposed Standard), July 2011
15.
Pnueli, A., Ruah, S., Zuck, L.D.: Automatic deductive verification with invisible invariants. In: Margaria, T., Yi, W. (eds.) TACAS 2001. LNCS, vol. 2031, p. 82. Springer, Heidelberg (2001) CrossRef
16.
Rodrigues, C.L., Guerra, F.V., de Figueiredo, J.C.A., Guerrero, D.D.S., Morais, T.S.: Modeling and verification of mobility issues using object-oriented petri nets. In: Proceedings of 3rd International Information and Telecommunication Technologies Symposium (I2TS2004) (2004)
17.
Zuck, L.D., Pnueli, A.: Model checking and abstraction to the aid of parameterized systems (a survey). Comput. Lang. Syst. Struct. 30(3–4), 139–169 (2004)MATH
Metadaten
Titel
Limited Mobility, Eventual Stability
verfasst von
Lenore D. Zuck
Sanjiva Prasad
Copyright-Jahr
2015
Buch
Hardware and Software: Verification and Testing

Print ISBN: 978-3-319-26286-4

Electronic ISBN: 978-3-319-26287-1

Copyright-Jahr: 2015

DOI
https://doi.org/10.1007/978-3-319-26287-1_9