Skip to main content
Disciplines
Automotive Business IT + Informatics Construction + Real Estate Electrical Engineering + Electronics Energy + Sustainability Insurance + Risk Finance + Banking Management + Leadership Marketing + Sales Mechanical Engineering + Materials
Events
DE
EN
Books
Journals
Topic Page
Marketing
Start single access now
Access for companies
EXTENDED SEARCH
Log in
Top
Published in:
Some Thoughts on Runtime Verification Read chapter Read first chapter

2016 | OriginalPaper | Chapter

Leveraging DTrace for Runtime Verification

Authors : Carl Martin Rosenberg, Martin Steffen, Volker Stolz

Published in: Runtime Verification

Publisher: Springer International Publishing

Log in

Activate our intelligent search to find suitable subject content or patents.

search-config
loading …

Abstract

DTrace, short for “dynamic tracing”, is a powerful diagnostic tool and tracing framework. It is invaluable for performance monitoring, tuning, and for getting insights into almost any aspect of a running system. In this paper we investigate how we can leverage the DTrace operating system-level instrumentation framework [9] to conduct runtime verification. To this end, we develop graphviz2dtrace, a tool for producing monitor scripts in DTrace’s domain-specific scripting language D for specification formulas written in \(\text{ LTL }_{3}\), a three-valued variety of the well-known Linear Temporal Logic. We evaluate the tool by analyzing a small stack-implementation and a multi-process system.

Dont have a licence yet? Then find out more about our products and how to get one now:

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!

inform now

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!

inform now

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!

inform now
previous chapter TrackOS: A Security-Aware Real-Time Operating System
next chapter Finite-Trace Linear Temporal Logic: Coinductive Completeness
Footnotes
2
The graphviz dot notation was chosen because LamaConv can produce it, for its ubiquity, and for the ease with which automata can be visualized.
 
Literature
1.
2.
3.
Barringer, H., Falcone, Y., Havelund, K., Reger, G., Rydeheard, D.: Quantified event automata: towards expressive and efficient runtime monitors. In: Giannakopoulou, D., Méry, D. (eds.) FM 2012. LNCS, vol. 7436, pp. 68–84. Springer, Heidelberg (2012)CrossRef
4.
Bauer, A., Leucker, M., Schallhart, C.: Model-based runtime analysis of distributed reactive systems. In: 17th Australian Software Engineering Conference (ASWEC 2006). IEEE Computer Society (2006)
5.
Bauer, A., Leucker, M., Schallhart, C.: Monitoring of real-time properties. In: Arun-Kumar, S., Garg, N. (eds.) FSTTCS 2006. LNCS, vol. 4337, pp. 260–272. Springer, Heidelberg (2006)CrossRef
6.
Bauer, A., Leucker, M., Schallhart, C.: Runtime verification for LTL and TLTL. ACM Trans. Softw. Eng. Methodol. 20(4), 1–64 (2011)CrossRef
7.
Bodden, E., Stolz, V.: Tracechecks: defining semantic interfaces with temporal logic. In: Löwe, W., Südholt, M. (eds.) SC 2006. LNCS, vol. 4089, pp. 147–162. Springer, Heidelberg (2006)CrossRef
8.
9.
Cantrill, B., Shapiro, M.W., Leventhal, A.H.: Dynamic instrumentation of production systems. In: ATEC 2004 Proceedings of the Annual Conference on USENIX Annual Technical Conference. USENIX (2004)
10.
Chachmon, N., Richins, D., Christensson, M., Cohn, R., Cui, W., Reddi, V.J.: Simulation and analysis engine for scale-out workloads. In: Proceedings of the 30th ACM on International Conference on Supercomputing. ACM (2016)
11.
Ellson, J., Gansner, E.R., Koutsofios, L., North, S.C., Woodhull, G.: Graphviz - open source graph drawing tools. In: Mutzel, P., Jünger, M., Leipert, S. (eds.) GD 2001. LNCS, vol. 2265, p. 483. Springer, Heidelberg (2002)CrossRef
12.
13.
Gregg, B., Mauro, J.: DTrace: Dynamic Tracing in Oracle Solaris, Mac OS X, and FreeBSD. Prentice Hall Professional, Upper Saddle River (2011)
14.
Havelund, K., Joshi, R.: Experience with rule-based analysis of spacecraft logs. In: Artho, C., Ölveczky, P.C. (eds.) FTSCS 2014. CCIS, vol. 476, pp. 1–16. Springer, Heidelberg (2015)
15.
16.
Laddad, R.: AspectJ in Action, 2nd edn. Manning Publications, Cherry Hill (2009)
17.
18.
Oracle Corporation: DTrace Guide for Oracle Solaris 11. Oracle Corporation, Redwood City (2012)
19.
20.
21.
Rosenberg, C.M.: Leveraging DTrace for runtime verification. Master thesis, Department of Informatics, Faculty of Mathematics and Natural Sciences, University of Oslo, May 2016
22.
23.
24.
Stolz, V., Bodden, E.: Temporal assertions using AspectJ. Electron. Notes Theoret. Comput. Sci. 144(4), 109–124 (2006)CrossRef
Metadata
Title
Leveraging DTrace for Runtime Verification
Authors
Carl Martin Rosenberg
Martin Steffen
Volker Stolz
Copyright Year
2016
Book
Runtime Verification

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

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

Copyright Year: 2016

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

Premium Partner

    Image Credits