Skip to main content

2017 | Supplement | Buchkapitel

Verifying the Output of a Distributed Algorithm Using Certification

verfasst von : Kim Völlinger

Erschienen in: Runtime Verification

Verlag: Springer International Publishing

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

search-config
loading …

Abstract

A certifying algorithm verifies the correctness of its output at runtime by producing a witness in addition to an input-output pair. If a witness predicate holds for the triple, the input-output pair is correct. A checker algorithm decides the witness predicate. While certifying sequential algorithms are well-established, we consider distributed algorithms. In this paper, we investigate certifying distributed algorithms that verify their distributed output. While the witness predicate states a property in the network, for distributed checking, additional predicates are decided for each component. We illustrate the applicability by examples.

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!

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!

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!

Fußnoten
1
For distributed algorithms, the global input is often the network itself.
 
Literatur
3.
Zurück zum Zitat Lynch, N.A.: Distributed Algorithms. Morgan Kaufmann Publishers Inc., San Francisco (1996)MATH Lynch, N.A.: Distributed Algorithms. Morgan Kaufmann Publishers Inc., San Francisco (1996)MATH
4.
Zurück zum Zitat McConnell, R.M., Mehlhorn, K., Näher, S., Schweitzer, P.: Certifying algorithms. Comput. Sci. Rev. 5, 119–161 (2011)CrossRefMATH McConnell, R.M., Mehlhorn, K., Näher, S., Schweitzer, P.: Certifying algorithms. Comput. Sci. Rev. 5, 119–161 (2011)CrossRefMATH
5.
Zurück zum Zitat Mostafa, M., Bonakdarpour, B.: Decentralized runtime verification of ltl specifications in distributed systems. In: Proceedings of the 2015 IEEE International Parallel and Distributed Processing Symposium, IPDPS 2015, pp. 494–503. IEEE Computer Society, Washington, DC (2015) Mostafa, M., Bonakdarpour, B.: Decentralized runtime verification of ltl specifications in distributed systems. In: Proceedings of the 2015 IEEE International Parallel and Distributed Processing Symposium, IPDPS 2015, pp. 494–503. IEEE Computer Society, Washington, DC (2015)
6.
Zurück zum Zitat Raynal, M.: Distributed Algorithms for Message-Passing Systems. Springer, Heidelberg (2013)CrossRefMATH Raynal, M.: Distributed Algorithms for Message-Passing Systems. Springer, Heidelberg (2013)CrossRefMATH
7.
Zurück zum Zitat Völlinger, K., Akili, S.: Verifying a class of certifying distributed programs. In: Barrett, C., Davies, M., Kahsai, T. (eds.) NFM 2017. LNCS, vol. 10227, pp. 373–388. Springer, Cham (2017). doi:10.1007/978-3-319-57288-8_27 CrossRef Völlinger, K., Akili, S.: Verifying a class of certifying distributed programs. In: Barrett, C., Davies, M., Kahsai, T. (eds.) NFM 2017. LNCS, vol. 10227, pp. 373–388. Springer, Cham (2017). doi:10.​1007/​978-3-319-57288-8_​27 CrossRef
8.
Zurück zum Zitat Völlinger, K., Reisig, W.: Certification of distributed algorithms solving problems with optimal substructure. In: Calinescu, R., Rumpe, B. (eds.) SEFM 2015. LNCS, vol. 9276, pp. 190–195. Springer, Cham (2015). doi:10.1007/978-3-319-22969-0_14 CrossRef Völlinger, K., Reisig, W.: Certification of distributed algorithms solving problems with optimal substructure. In: Calinescu, R., Rumpe, B. (eds.) SEFM 2015. LNCS, vol. 9276, pp. 190–195. Springer, Cham (2015). doi:10.​1007/​978-3-319-22969-0_​14 CrossRef
Metadaten
Titel
Verifying the Output of a Distributed Algorithm Using Certification
verfasst von
Kim Völlinger
Copyright-Jahr
2017
DOI
https://doi.org/10.1007/978-3-319-67531-2_29