Leveraging DTrace for Runtime Verification

Abstract

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 which 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.