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:
Analyzing Array Manipulating Programs by Program Transformation Kapitel lesen Erstes Kapitel lesen

2015 | OriginalPaper | Buchkapitel

A Hybrid Method for the Verification and Synthesis of Parameterized Self-Stabilizing Protocols

verfasst von : Amer Tahat, Ali Ebnenasir

Erschienen in: Logic-Based Program Synthesis and Transformation

Verlag: Springer International Publishing

Einloggen

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

search-config
loading …

Abstract

This paper presents a hybrid method for verification and synthesis of parameterized self-stabilizing protocols where algorithmic design and mechanical verification techniques/tools are used hand-in-hand. The core idea behind the proposed method includes the automated synthesis of self-stabilizing protocols in a limited scope (i.e., fixed number of processes) and the use of theorem proving methods for the generalization of the solutions produced by the synthesizer. Specifically, we use the Prototype Verification System (PVS) to mechanically verify an algorithm for the synthesis of weakly self-stabilizing protocols. Then, we reuse the proof of correctness of the synthesis algorithm to establish the correctness of the generalized versions of synthesized protocols for an arbitrary number of processes. We demonstrate the proposed approach in the context of an agreement and a coloring protocol on the ring topology.

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 Liveness Properties in CafeOBJ – A Case Study for Meta-Level Specifications
Nächstes Kapitel Drill and Join: A Method for Exact Inductive Program Synthesis
Literatur
1.
Abdulla, P.A., Jonsson, B.: Model checking of systems with many identical timed processes. Theor. Comput. Sci. 290(1), 241–264 (2003)CrossRefMATHMathSciNet
2.
Abdulla, P.A., Jonsson, B., Nilsson, M., Saksena, M.: A survey of regular model checking. In: Gardner, P., Yoshida, N. (eds.) CONCUR 2004. LNCS, vol. 3170, pp. 35–48. Springer, Heidelberg (2004) CrossRef
3.
Abujarad, F., Kulkarni, S.S.: Multicore constraint-based automated stabilization. In: Guerraoui, R., Petit, F. (eds.) SSS 2009. LNCS, vol. 5873, pp. 47–61. Springer, Heidelberg (2009) CrossRef
4.
Abujarad, F., Kulkarni, S.S.: Automated constraint-based addition of nonmasking and stabilizing fault-tolerance. Theor. Comput. Sci. 412(33), 4228–4246 (2011)CrossRefMATHMathSciNet
5.
Arora, A., Gouda, M.G.: Closure and convergence: a foundation of fault-tolerant computing. IEEE Trans. Softw. Eng. 19(11), 1015–1027 (1993)CrossRef
6.
Attie, P.C., Arora, A., Emerson, E.A.: Synthesis of fault-tolerant concurrent programs. ACM Trans. Program. Lang. Syst (TOPLAS) 26(1), 125–185 (2004)CrossRef
7.
Bertrand, N., Fournier, P.: Parameterized verification of many identical probabilistic timed processes. In: LIPIcs-Leibniz International Proceedings in Informatics, vol. 24 (2013)
8.
Bonakdarpour, B., Kulkarni, S.S.: Towards reusing formal proofs for verification of fault-tolerance. In Workshop in Automated Formal Methods (2006)
9.
Bouajjani, A., Jonsson, B., Nilsson, M., Touili, T.: Regular model checking. In: Emerson, E.A., Sistla, A.P. (eds.) CAV 2000. LNCS, vol. 1855, pp. 403–418. Springer, Heidelberg (2000) CrossRef
10.
Dijkstra, E.W.: Self-stabilizing systems in spite of distributed control. Commun. ACM 17(11), 643–644 (1974)CrossRefMATH
11.
Dolev, S., Haviv, Y.A.: Self-stabilizing microprocessor: analyzing and overcoming soft errors. IEEE Trans. Comput. 55(4), 385–399 (2006)CrossRef
12.
Dolev, S., Yagel, R.: Self-stabilizing operating systems. In: Proceedings of the twentieth ACM symposium on Operating systems principles, pages 1–2. ACM (2005)
13.
Ebnenasir, A., Farahat, A.: Swarm synthesis of convergence for symmetric protocols. In: European Dependable Computing Conference, pp. 13–24 (2012)
14.
Ebnenasir, A., Kulkarni, S.S., Arora, A.: FTSyn: a framework for automatic synthesis of fault-tolerance. Int. J. Softw. Tools Technol. Transf. 10(5), 455–471 (2008)CrossRef
15.
16.
Farahat, A., Ebnenasir, A.: A lightweight method for automated design of convergence in network protocols. ACM Trans. Auton. Adapt. Syst. (TAAS) 7(4), 38:1–38:36 (2012)
17.
Fioravanti, F., Pettorossi, A., Proietti, M., Senni, V.: Generalization strategies for the verification of infinite state systems. TPLP 13(2), 175–199 (2013)MATHMathSciNet
18.
Gordon, M.J.C., Melham, T.F.: Introduction to HOL: A Theorem proving Environment for Higher Order Logic. Cambridge University Press, Cambridge (1993) MATH
19.
Gouda, M.G.: The theory of weak stabilization. In: Datta, A.K., Herman, T. (eds.) WSS 2001. LNCS, vol. 2194, p. 114. Springer, Heidelberg (2001) CrossRef
20.
Grinchtein, O., Leucker, M., Piterman, N.: Inferring network invariants automatically. In: Furbach, U., Shankar, N. (eds.) IJCAR 2006. LNCS (LNAI), vol. 4130, pp. 483–497. Springer, Heidelberg (2006) CrossRef
21.
Ip, C.N., Dill, D.L.: Verifying systems with replicated components in murphi. Form. Methods Syst. Design 14(3), 273–310 (1999)CrossRef
22.
Jacobs, S., Bloem, R.: Parameterized synthesis. In: Flanagan, C., König, B. (eds.) TACAS 2012. LNCS, vol. 7214, pp. 362–376. Springer, Heidelberg (2012) CrossRef
23.
Kesten, Y., Pnueli, A., Shahar, E., Zuck, L.D.: Network invariants in action. In: Brim, L., Jančar, P., Křetínský, M., Kučera, A. (eds.) CONCUR 2002. LNCS, vol. 2421, pp. 101–115. Springer, Heidelberg (2002) CrossRef
24.
Khalimov, A., Jacobs, S., Bloem, R.: PARTY Parameterized Synthesis of Token Rings. In: Sharygina, N., Veith, H. (eds.) CAV 2013. LNCS, vol. 8044, pp. 928–933. Springer, Heidelberg (2013) CrossRef
25.
26.
Klinkhamer, A., Ebnenasir, A.: On the complexity of adding convergence. In: Arbab, F., Sirjani, M. (eds.) FSEN 2013. LNCS, vol. 8161, pp. 17–33. Springer, Heidelberg (2013) CrossRef
27.
Kulkarni, S.S., Arora, A.: Large automating the addition of fault-tolerance. In: Joseph, M. (ed.) FTRTFT 2000. LNCS, vol. 1926, p. 82. Springer, Heidelberg (2000) CrossRef
28.
Kulkarni, S.S., Bonakdarpour, B., Ebnenasir, A.: Mechanical verification of automatic synthesis of fault-tolerance. Int. Symp. Log.-based Program Synth. Transform. 3573, 36–52 (2004)MathSciNet
29.
Kulkarni, S.S., Rushby, J., Shankar, N.: A case-study in component-based mechanical verification of fault-tolerant programs. In: 19th IEEE International Conference on Distributed Computing Systems - Workshop on Self-Stabilizing Systems, pp. 33–40 (1999)
30.
Pnueli, A., Xu, J., Zuck, L.D.: Liveness with \({(0,1,\infty )}\)-Counter Abstraction. In: Brinksma, Ed, Larsen, Kim Guldstrand (eds.) CAV 2002. LNCS, vol. 2404, pp. 107–. Springer, Heidelberg (2002)
31.
Prasetya, I.S.W.B.: Mechanically verified self-stabilizing hierarchical algorithms. Tools and Algorithms for the Construction and Analysis of Systems (TACAS’97), volume 1217 of Lecture Notes in Computer Science, pages 399–415 (1997)
32.
Qadeer, S., Shankar, N.: Verifying a self-stabilizing mutual exclusion algorithm. In: Gries, D., de Roever, W.-P. (eds.) IFIP International Conference on Programming Concepts and Methods (PROCOMET 1998), pp. 424–443. Chapman & Hall, Shelter Island, NY (1998) CrossRef
33.
Roychoudhury, A., Narayan Kumar, K., Ramakrishnan, C.R., Ramakrishnan, I.V., Smolka, S.A.: Verification of Parameterized Systems Using Logic Program Transformations. In: Graf, S. (ed.) TACAS 2000. LNCS, vol. 1785, p. 172. Springer, Heidelberg (2000) CrossRef
34.
Shankar, N., Owre, S., Rushby, J.M.: The PVS Proof Checker: A Reference Manual. Computer Science Laboratory, SRI International, Menlo Park, CA, Feb. 1993. A new edition for PVS Version 2 is released in 1998
35.
36.
Tsuchiya, T., Nagano, S., Paidi, R.B., Kikuno, T.: Symbolic model checking for self-stabilizing algorithms. IEEE Trans. Parallel Distrib. Syst. 12(1), 81–95 (2001)CrossRef
37.
Wolper, P., Lovinfosse, V.: Verifying properties of large sets of processes with network invariants. In: International Workshop on Automatic Verification Methods for Finite State Systems, pp. 68–80 (1989)
Metadaten
Titel
A Hybrid Method for the Verification and Synthesis of Parameterized Self-Stabilizing Protocols
verfasst von
Amer Tahat
Ali Ebnenasir
Copyright-Jahr
2015
Buch
Logic-Based Program Synthesis and Transformation

Print ISBN: 978-3-319-17821-9

Electronic ISBN: 978-3-319-17822-6

Copyright-Jahr: 2015

DOI
https://doi.org/10.1007/978-3-319-17822-6_12