DSL-based Runtime Verification for the JVM

The author of this thesis is Christian Pohlmann.

This thesis is concerned with the development of runtime verification frameworks
while putting particular emphasis on how events and correctness properties
can be declared. A runtime verification framework called Flens (Functional logic
evaluation and notification system) written in Clojure, a member of the Lisp family
of languages, was developed including a domain-specific language for event and
property declaration.
After quickly introducing the goal of this thesis and providing relevant background
information on runtime verification needed for later chapters, fundamental
language features of Lisp-like languages and the development of domainspecific
languages in Clojure are discussed.
The design and architecture of Flens is then introduced, while specific design decisions
are compared to alternative approaches. A method of parsing LTL formulae
is presented by applying Dijkstra’s shunting yard algorithm to s-expressions, rendering
common solutions such as parser generators and combinators unnecessary.
The question how to map elements from theory to practical applications is dealt
with extensively in this thesis, in particular how to represent atomic propositions
as events and how to find a sound concept of time. It is shown that uncoupling
time and events is of vital importance to ensure a consistent behaviour.
Both a formulra-rewriting approach as well as an automata-based approach are
discussed and compared.