Nettsider med emneord «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.

Runtime verification uses techniques from formal methods such as temporal logics and regular expressions to monitor software execution. In this thesis, we investigate new possibilities to combine this technique with formal specifications of correctness and performance properties.