Leveraging DTrace for Runtime Verification

by Carl Martin Rosenberg

As we create increasingly complex software systems, we need better tools and concepts to analyze and understand them. On the practical level, we need instrumentation tools that give insights into running systems in a safe and efficient manner. On the analytical level, we need better ways of reasoning about systems as their state and behavior change over time. Runtime verification is an emergent field of research that studies how to rigorously specify properties about software systems and how corresponding monitors – programs that check if the system satisfies these properties – can be built. In this thesis, we investigate how we can leverage the DTrace instrumentation framework to conduct runtime verification. To this end, we develop graphviz2dtrace, a tool for producing monitor scripts in DTrace's domain-specific scripting language D from specification formulas written in LTL3, a three-valued variety of the well-known Linear Temporal Logic. We evaluate the tool by analyzing both single- and multi process systems.

Demonstration screencasts

graphviz2dtrace demo: The Stack from Carl Martin Rosenberg on Vimeo.

graphviz2dtrace demo: Node.js + PostgreSQL from Carl Martin Rosenberg on Vimeo.

Published June 6, 2016 1:44 AM - Last modified Apr. 13, 2018 10:32 AM