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

Antriebe und Energiesysteme von morgen


Austausch von Automobil- und Energiewirtschaft

Am 14./15. Mai geht es in Chemnitz um die Mobilitätswende durch Elektro- und Wasserstofffahrzeuge.
Erweiterte Suche
Anmelden
nach oben
International Journal on Software Tools for Technology Transfer
Erschienen in: International Journal on Software Tools for Technology Transfer 2/2016

01.04.2016 | TACAS 2014

Monitoring modulo theories

verfasst von: Normann Decker, Martin Leucker, Daniel Thoma

Erschienen in: International Journal on Software Tools for Technology Transfer | Ausgabe 2/2016

Einloggen

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

search-config
loading …

Abstract

This paper considers a generic approach to runtime verification of temporal properties over first-order theories. This allows especially for the verification of multi-threaded, object-oriented systems. It presents a general framework lifting monitor synthesis procedures for propositional temporal logics to a temporal logic over structures within some first-order theory. To evaluate such specifications SMT solving and classical monitoring of propositional temporal properties are combined. The monitoring procedure was implemented for linear-time temporal logic based on the Z3 SMT solver and evaluated regarding runtime performance.
Vorheriger Artikel SATMC: a SAT-based model checker for security protocols, business processes, and security APIs
Nächster Artikel Probabilistic verification and synthesis of the next generation airborne collision avoidance system

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
Fußnoten
2
The benchmarks and corresponding implementation are available at http://​www.​isp.​uni-luebeck.​de/​~thoma/​junitrv-sttt14.​zip.
 
Literatur
1.
Allan, C., Avgustinov, P., Christensen, A.S., Hendren, L.J., Kuzins, S., Lhoták, O., de Moor, O., Sereni, D., Sittampalam, G., Tibble, J.: Adding trace matching with free variables to aspectj. In: Johnson, R.E., Gabriel, R.P. (eds.) Proceedings of the 20th Annual ACM SIGPLAN Conference on Object-Oriented Programming, Systems, Languages, and Applications, OOPSLA 2005, San Diego, pp. 345–364. ACM (2005)
2.
Alur, R., Etessami, K., Madhusudan, P.: A temporal logic of nested calls and returns. In: Jensen, K., Podelski, A. (eds.) Tools and Algorithms for the Construction and Analysis of Systems, 10th International Conference, TACAS 2004, Held as Part of the Joint European Conferences on Theory and Practice of Software, ETAPS 2004, Barcelona, Proceedings, Lecture Notes in Computer Science, vol. 2988, pp. 467–481. Springer, Berlin (2004)
3.
Biere, A., Clarke, E.M., Raimi, R., Zhu, Y.: Verifiying safety properties of a power PC microprocessor using symbolic model checking without bdds. In: Halbwachs, N., Peled, D. (eds.) Computer Aided Verification, 11th International Conference, CAV ’99, Trento, Proceedings, Lecture Notes in Computer Science, vol. 1633, pp. 60–71. Springer, Berlin (1999)
4.
Barringer, H., Falcone, Y., Havelund, K., Reger, G., Rydeheard, D.E.: Quantified event automata: Towards expressive and efficient runtime monitors. In: Giannakopoulou, D., Méry, D. (eds.) FM 2012: Formal Methods—18th International Symposium, Paris, Proceedings, Lecture Notes in Computer Science, vol. 7436, pp. 68–84. Springer, Berlin (2012)
5.
Barringer, H., Goldberg, A., Havelund, K., Sen, K.: Rule-based runtime verification. In: Steffen, B., Levi, G. (eds.) Verification, Model Checking, and Abstract Interpretation, 5th International Conference, VMCAI 2004, Venice, Proceedings, Lecture Notes in Computer Science, vol. 2937, pp. 44–57. Springer, Berlin (2004)
6.
Backasch, R., Hochberger, C., Weiss, A., Leucker, M., Lasslop, R.: Runtime verification for multicore soc with high-quality trace data. ACM Trans. Design Autom. Electron. Syst. 18(2), 18 (2013)CrossRef
7.
Broy, M., Jonsson, B., Katoen, J.-P., Leucker, M., Pretschner, A. (eds.) Model-Based Testing of Reactive Systems, Advanced Lectures (the volume is the outcome of a research seminar that was held in Schloss Dagstuhl in January 2004), Lecture Notes in Computer Science, vol. 3472. Springer, Berlin (2005)
8.
Basin, D.A., Klaedtke, F., Müller, S.: Policy monitoring in first-order temporal logic. In: Touili, T., Cook, B., Jackson, P. (eds.) Computer Aided Verification, 22nd International Conference, CAV 2010, Edinburgh, Proceedings, Lecture Notes in Computer Science, vol. 6174, pp. 1–18. Springer, Berlin (2010)
9.
Bauer, A., Küster, J.-C., Vegliach, G.: From propositional to first-order monitoring. In: Legay, A., Bensalem, S. (eds.) Runtime Verification—4th International Conference, RV 2013, Rennes, Proceedings, Lecture Notes in Computer Science, vol. 8174, pp. 59–75. Springer, Berlin (2013)
10.
Bauer, A., Leucker, M., Schallhart, C.: Monitoring of real-time properties. In: Arun-Kumar, S., Garg, N. (eds.) FSTTCS 2006: Foundations of Software Technology and Theoretical Computer Science, 26th International Conference, Kolkata, Proceedings, Lecture Notes in Computer Science, vol. 4337, pp. 260–272. Springer, Berlin (2006)
11.
Bauer, A., Leucker, M., Schallhart, C.: The good, the bad, and the ugly, but how ugly is ugly? In: Sokolsky, O., Tasiran, S. (eds.) Runtime Verification, 7th International Workshop, RV 2007, Vancouver, Revised Selected Papers, Lecture Notes in Computer Science, vol. 4839, pp. 126–138. Springer, Berlin (2007)
12.
Bauer, A., Leucker, M., Schallhart, C.: Runtime verification for LTL and TLTL. ACM Trans. Softw. Eng. Methodol. 20(4), 14 (2011)CrossRef
13.
Barringer, H., Rydeheard, D.E., Havelund, K.: Rule systems for run-time monitoring: from eagleto ruler. In: Sokolsky, O., Tasiran, S. (eds.) Runtime Verification, 7th International Workshop, RV 2007, Vancouver, Revised Selected Papers, Lecture Notes in Computer Science, vol. 4839, pp. 111–125. Springer, Berlin (2007)
14.
Clarke, E.M., Grumberg, O., Peled, D.: Model Checking. MIT Press, Massachusetts (2001)CrossRef
15.
Colombo, C., Pace, G.J., Schneider, G.: LARVA—safer monitoring of real-time java programs (tool paper). In: Van Hung, D., Krishnan, P. (eds.) Seventh IEEE International Conference on Software Engineering and Formal Methods, SEFM 2009, Hanoi, , pp. 33–37. IEEE Computer Society (2009)
16.
Chen, F., Rosu, G.: Java-mop: a monitoring oriented programming environment for java. In: Halbwachs, N., Zuck, L.D. (eds.) Tools and Algorithms for the Construction and Analysis of Systems, 11th International Conference, TACAS 2005, Held as Part of the Joint European Conferences on Theory and Practice of Software, ETAPS 2005, Edinburgh, Proceedings, Lecture Notes in Computer Science, vol. 3440, pp. 546–550. Springer, Berlin (2005)
17.
Chen, F., Rosu, G.: Parametric trace slicing and monitoring. In: Kowalewski, S., Philippou, A. (eds.) Tools and Algorithms for the Construction and Analysis of Systems, 15th International Conference, TACAS 2009, Held as Part of the Joint European Conferences on Theory and Practice of Software, ETAPS 2009, York, Proceedings, Lecture Notes in Computer Science, vol. 5505, pp. 246–261. Springer, Berlin (2009)
18.
Decker, N., Kühn, F., Thoma, D.: Runtime verification of web services for interconnected medical devices. In: 25th IEEE International Symposium on Software Reliability Engineering, ISSRE 2014, Naples, pp. 235–244. IEEE (2014)
19.
Dong, W., Leucker, M., Schallhart, C.: Impartial anticipation in runtime-verification. In: Cha, S.D., Choi, J.-Y., Kim, M., Lee, I., Viswanathan, M. (eds.) Automated Technology for Verification and Analysis, 6th International Symposium, ATVA 2008, Seoul, Proceedings, Lecture Notes in Computer Science, vol. 5311, pp. 386–396. Springer, Berlin (2008)
20.
Decker, N., Leucker, M., Thoma, D.: Impartiality and anticipation for monitoring of visibly context-free properties. In: Legay, A., Bensalem, S. (eds.) Runtime Verification—4th International Conference, RV 2013, Rennes, Proceedings, Lecture Notes in Computer Science, vol. 8174, pp. 183–200. Springer, Berlin (2013)
21.
Decker, N., Leucker, M., Thoma, D.: junit\(^{{\rm rv}}\)-adding runtime verification to junit. In: Brat, G., Rungta, N., Venet, A. (eds.) NASA Formal Methods, 5th International Symposium, NFM 2013, Moffett Field, Proceedings, Lecture Notes in Computer Science, vol. 7871, pp. 459–464. Springer, Berlin (2013)
22.
Decker, N., Leucker, M., Thoma, D.: Monitoring modulo theories. In: Ábrahám, E., Havelund, K. (eds.) Tools and Algorithms for the Construction and Analysis of Systems—20th International Conference, TACAS 2014, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2014, Grenoble, Proceedings, Lecture Notes in Computer Science, vol. 8413, pp. 341–356. Springer, Berlin (2014)
23.
de Moura, L.M., Bjørner, N.: Z3: an efficient SMT solver. In: Ramakrishnan, C.R., Rehof, J. (eds.) Tools and Algorithms for the Construction and Analysis of Systems, 14th International Conference, TACAS 2008, Held as Part of the Joint European Conferences on Theory and Practice of Software, ETAPS 2008, Budapest, Proceedings, Lecture Notes in Computer Science, vol. 4963, pp. 337–340. Springer, Berlin (2008)
24.
de Moura, L.M., Bjørner, N.: Satisfiability modulo theories: introduction and applications. Commun. ACM 54(9), 69–77 (2011)CrossRef
25.
Ebbinghaus, H.-D., Flum, J., Thomas, W.: Mathematical Logic, 2nd edn. Undergraduate Texts in Mathematics. Springer, Berlin (1994)CrossRef
26.
Forgy, C.: Rete: a fast algorithm for the many patterns/many objects match problem. Artif. Intell. 19(1), 17–37 (1982)CrossRef
27.
Havelund, Klaus: Monitoring with data automata. In: Margaria, Tiziana, Steffen, Bernhard (eds.) Leveraging Applications of Formal Methods, Verification and Validation. Specialized Techniques and Applications—6th International Symposium, ISoLA 2014, Imperial, Corfu, Proceedings, Part II, Lecture Notes in Computer Science, vol. 8803, pp. 254–273. Springer, Berlin (2014)
28.
Havelund, K.: Rule-based runtime verification revisited. STTT 17(2), 143–170 (2015)CrossRef
29.
Leucker, M., Sánchez, C.: Regular linear temporal logic. In: Jones, C.B., Liu, Z., Woodcock, J. (eds.) Theoretical Aspects of Computing—ICTAC 2007, 4th International Colloquium, Macau, Proceedings, Lecture Notes in Computer Science, vol. 4711, pp. 291–305. Springer, Berlin (2007)
30.
Leucker, M., Schallhart, C.: A brief account of runtime verification. J. Log. Algebr. Program. 78(5), 293–303 (2009)CrossRefMATH
31.
Meredith, P.O.N., Jin, D., Griffith, D., Chen, F., Rosu, G.: An overview of the MOP runtime verification framework. STTT 14(3), 249–289 (2012)CrossRef
32.
Stolz, V., Bodden, E.: Temporal assertions using aspectj. Electron. Notes Theor. Comput. Sci. 144(4), 109–124 (2006)CrossRef
33.
Stolz, V.: Temporal assertions with parametrized propositions. J. Log. Comput. 20(3), 743–757 (2010)
Metadaten
Titel
Monitoring modulo theories
verfasst von
Normann Decker
Martin Leucker
Daniel Thoma
Publikationsdatum
01.04.2016
Verlag
Springer Berlin Heidelberg
Erschienen in
International Journal on Software Tools for Technology Transfer / Ausgabe 2/2016
Print ISSN: 1433-2779
Elektronische ISSN: 1433-2787
DOI
https://doi.org/10.1007/s10009-015-0380-3

Weitere Artikel der Ausgabe 2/2016

International Journal on Software Tools for Technology Transfer 2/2016 Zur Ausgabe

TACAS 2014

Probabilistic verification and synthesis of the next generation airborne collision avoidance system

TACAS 2014

Some recent advances in automated analysis

TACAS 2014

Concurrent depth-first search algorithms based on Tarjan’s Algorithm

Tacas 2014

SATMC: a SAT-based model checker for security protocols, business processes, and security APIs

TACAS 2014

Many-core on-the-fly model checking of safety properties using GPUs

TACAS 2014

FDR3: a parallel refinement checker for CSP

Premium Partner

    Bildnachweise