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:
Some Thoughts on Runtime Verification Kapitel lesen Erstes Kapitel lesen

2016 | OriginalPaper | Buchkapitel

Accelerated Runtime Verification of LTL Specifications with Counting Semantics

verfasst von : Ramy Medhat, Borzoo Bonakdarpour, Sebastian Fischmeister, Yogi Joshi

Erschienen in: Runtime Verification

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 novel and efficient parallel algorithm for runtime verification of an extension of Ltl that allows for nested quantifiers subject to numerical constraints. Such constraints are useful in evaluating thresholds (e.g., expected uptime of a web server). Our algorithm uses the MapReduce programming model to split a program trace into variable-based clusters at run time. Each cluster is then mapped to its respective monitor instances, verified, and reduced collectively on a multi-core CPU or the GPU. Our experiments on real-world case studies show that the algorithm imposes negligible monitoring overhead.

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 nfer – A Notation and System for Inferring Event Stream Abstractions
Nächstes Kapitel Non-intrusive Runtime Monitoring Through Power Consumption: A Signals and System Analysis Approach to Reconstruct the Trace
Literatur
1.
Barre, B., Klein, M., Soucy-Boivin, M., Ollivier, P.-A., Hallé, S.: MapReduce for Parallel trace validation of LTL properties. In: Qadeer, S., Tasiran, S. (eds.) RV 2012. LNCS, vol. 7687, pp. 184–198. Springer, Heidelberg (2013). doi:10.​1007/​978-3-642-35632-2_​20 CrossRef
2.
Barringer, H., Goldberg, A., Havelund, K., Sen, K.: Program monitoring with LTL in eagle. In: 2004 Proceedings of the 18th International Parallel and Distributed Processing Symposium, p. 264. IEEE (2004)
3.
Basin, D., Caronni, G., Ereth, S., Harvan, M., Klaedtke, F., Mantel, H.: Scalable offline monitoring. In: Bonakdarpour, B., Smolka, S.A. (eds.) RV 2014. LNCS, vol. 8734, pp. 31–47. Springer, Heidelberg (2014). doi:10.​1007/​978-3-319-11164-3_​4
4.
Basin, D., Klaedtke, F., Marinovic, S., Zălinescu, E.: Monitoring of temporal first-order properties with aggregations. Formal Methods Syst. Des. 46(3), 262–285 (2015)CrossRefMATH
5.
Bauer, A., Küster, J.-C., Vegliach, G.: From propositional to first-order monitoring. In: Legay, A., Bensalem, S. (eds.) RV 2013. LNCS, vol. 8174, pp. 59–75. Springer, Heidelberg (2013)CrossRef
6.
Bauer, A., Leucker, M., Schallhart, C.: Comparing LTL semantics for runtime verification. J. Logic Comput. 20(3), 651–674 (2010)MathSciNetCrossRefMATH
7.
Berkovich, S., Bonakdarpour, B., Fischmeister, S.: GPU-based runtime verification. In: IEEE International Parallel and Distributed Processing Symposium (IPDPS), pp. 1025–1036 (2013)
8.
Berkovich, S., Bonakdarpour, B., Fischmeister, S.: Runtime verification with minimal intrusion through parallelism. Formal Methods Syst. Des. 46(3), 317–348 (2015)CrossRefMATH
9.
Chen, F., Roşu, G.: Parametric trace slicing and monitoring. In: Kowalewski, S., Philippou, A. (eds.) TACAS 2009. LNCS, vol. 5505, pp. 246–261. Springer, Heidelberg (2009)CrossRef
10.
d’Angelo, B., Sankaranarayanan, S., Sánchez, C., Robinson, W., Finkbeiner, B., Sipma, H.B., Mehrotra, S., Manna, Z.: LOLA: runtime monitoring of synchronous systems. In: 12th International Symposium on Temporal Representation and Reasoning (TIME 2005), pp. 166–174. IEEE (2005)
11.
Decker, N., Leucker, M., Thoma, D.: Monitoring modulo theories. In: Ábrahám, E., Havelund, K. (eds.) TACAS 2014 (ETAPS). LNCS, vol. 8413, pp. 341–356. Springer, Heidelberg (2014)CrossRef
12.
Drago, I., Mellia, M., Munafo, M.M., Sperotto, A., Sadre, R., Pras, A.: Inside dropbox: understanding personal cloud storage services. In: Proceedings of the 2012 ACM Conference on Internet Measurement Conference, pp. 481–494. ACM (2012)
13.
Jin, D., Meredith, P.O., Lee, C., Rosu, G.: JavaMOP: efficient parametric runtime monitoring framework. In: 2012 34th International Conference on Software Engineering (ICSE), pp. 1427–1430, June 2012
14.
Laroussinie, F., Meyer, A., Petonnet, E.: Counting LTL. In; Proceedings of the 2010 17th International Symposium on Temporal Representation and Reasoning, TIME 2010, pp. 51–58. IEEE Computer Society, Washington, DC (2010)
15.
16.
Meredith, P., Rosu, G.: Efficient parametric runtime verification with deterministic string rewriting. In: 2013 IEEE/ACM 28th International Conference on Automated Software Engineering (ASE), pp. 70–80. IEEE (2013)
17.
Navabpour, S., Joshi, Y., Wu, W., Berkovich, S., Medhat, R., Bonakdarpour, B., Fischmeister, S.: RiTHM: a tool for enabling time-triggered runtime verification for C programs. In: ACM Symposium on the Foundations of Software Engineering (FSE), pp. 603–606 (2013)
18.
Sokolsky, O., Sammapun, U., Lee, I., Kim, J.: Run-time checking of dynamic properties. Electron. Notes Theoret. Comput. Sci. 144(4), 91–108 (2006)CrossRef
19.
20.
Zink, M., Suh, K., Gu, Y., Kurose, J.: Watch global, cache local: Youtube network traffic at a campus network: measurements and implications. In: Electronic Imaging 2008, p. 681805. International Society for Optics and Photonics (2008)
Metadaten
Titel
Accelerated Runtime Verification of LTL Specifications with Counting Semantics
verfasst von
Ramy Medhat
Borzoo Bonakdarpour
Sebastian Fischmeister
Yogi Joshi
Copyright-Jahr
2016
Buch
Runtime Verification

Print ISBN: 978-3-319-46981-2

Electronic ISBN: 978-3-319-46982-9

Copyright-Jahr: 2016

DOI
https://doi.org/10.1007/978-3-319-46982-9_16