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
ATZ-Fachkongress

Chassis.tech plus 2024


4 Kongresse in einer Veranstaltung

Treffen Sie in München die Fachleute von Chassis, Lenkung, Bremsen sowie Reifen/Räder.
Erweiterte Suche
Anmelden
nach oben
Erschienen in:
Automating Abstract Interpretation Kapitel lesen Erstes Kapitel lesen

2016 | OriginalPaper | Buchkapitel

Cloud-Based Verification of Concurrent Software

verfasst von : Gerard J. Holzmann

Erschienen in: Verification, Model Checking, and Abstract Interpretation

Verlag: Springer Berlin Heidelberg

Einloggen

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

search-config
loading …

Abstract

Logic model checkers are unparalleled in their ability to reveal subtle bugs in multi-threaded software systems. The underlying verification procedure is based on a systematic search of potentially faulty system behaviors, which can be computationally expensive for larger problem sizes. In this paper we consider if it is possible to significantly reduce the runtime requirements of a verification with cloud computing techniques. We explore the use of large numbers of CPU-cores, that each perform small, fast, independent, and randomly different searches to achieve the same problem coverage as a much slower stand-alone run on a single CPU. We present empirical results to demonstrate what is achievable.

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 Hybrid Analysis for Partial Order Reduction of Programs with Arrays
Nächstes Kapitel Abstraction-driven Concolic Testing
Anhänge
Nur mit Berechtigung zugänglich
Literatur
1.
Bloom, B.H.: Space/Time trade-offs in hash coding with allowable errors. Comm. ACM 13(7), 422–426 (1970)MATHCrossRef
2.
Adsul, B., Flood, C.H., Garthwaite, A.T., Martin, P.A., Shavit, N.N., Steele Jr., G.L.: Even better DCAS-based concurrent deques. In: Herlihy, M.P. (ed.) DISC 2000. LNCS, vol. 1914, pp. 59–73. Springer, Heidelberg (2000) CrossRef
3.
Doherty, S., Detlefs, D.L., Groves, L., et al.: DCAS is not a silver bullet for nonblocking algorithm design. In: Gibbons, P.B., Adler, M. (eds.) Proceedings of Sixteenth Annual ACM Symposium on Parallel Algorithms, pp. 216–224, Barcelona (2004)
4.
Dwyer, M.B., Elbaum, S.G., et al.: Parallel randomized state-space search. In: Proceedings of ICSE 2007, pp. 3–12 (2007)
5.
Havelund, K.: Mechanical verification of a garbage collector. In: Proceedings of International Workshop on High-Level Parallel Programming Models and Supportive Environments, pp. 1258–1283, Puerto Rico (1999)
6.
Holzmann, G.J.: On limits and possibilities of automated protocol analysis. In: Proceedings of 6th International Conference on Protocol Specification, Testing and Verification INWG IFIP, pp. 339–344 (1987)
7.
Holzmann, G.J., Smith, M.H.: Automating software feature verification. Bell Labs Tech. J. 5(2), 72–87 (2000). Special Issue on Software ComplexityCrossRef
8.
Holzmann, G.J.: The Spin Model Checker - Primer and Reference Manual. Addison-Wesley, Reading (2004)
9.
Holzmann, G.J., Joshi, R., Groce, A.: Swarm verification techniques. IEEE Trans. Softw. Eng. 37(6), 845–857 (2011)CrossRef
10.
Holzmann, G.J., Florian, M.: Model checking with bounded context switching. Formal Aspects Comput. 23(3), 365–389 (2001)CrossRef
11.
12.
13.
Joshi, R., Holzmann, G.J.: A mini challenge: build a verifiable filesystem. In: Proceedings of Verified Software: Theories, Tools, Experiments, Formal Aspects of Computing, vol. 19(2), pp. 269–272 (2007)
14.
15.
Penix, J., Visser, W., Pasareanu, C., et al.: Verifying time partitioning in the DEOS scheduling kernel. Formal Meth. Syst. Des. J. 26(2), 103–135 (2005)MATHCrossRef
16.
17.
Metadaten
Titel
Cloud-Based Verification of Concurrent Software
verfasst von
Gerard J. Holzmann
Copyright-Jahr
2016
Verlag
Springer Berlin Heidelberg
Buch
Verification, Model Checking, and Abstract Interpretation

Print ISBN: 978-3-662-49121-8

Electronic ISBN: 978-3-662-49122-5

Copyright-Jahr: 2016

DOI
https://doi.org/10.1007/978-3-662-49122-5_15

Premium Partner

    Bildnachweise