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.
- Thesis document page at DUO
- Programs and run data discussed in the thesis
- graphviz2dtrace repository
- Presentation slides (PDF)