Runtime Verification of Real Time Properties and Bounded Model Checking in the Thorium Reactive Programming Language

Writing software that reacts to external events in real time is notoriously difficult. Some of that difficulty comes from the languages and frameworks that we use to write that software and I argue that a declarative language can mitigate some of that challenge by ensuring that the full definition of each reactive element exists in only one place in the code. To support real time specifications, we introduce a novel monitoring algorithm for several useful subsets of Metric Temporal Logic (MTL) and describe the time and space complexity of each. We then embed the monitor for the past-time subset -- due to its linear space and time complexity as well as the guarantee of timely results -- into a declarative reactive framework so that a programmer can define real time properties and respond if they are violated. Finally, we present a declarative language, textit{thorium}, for defining reactive software. It employs many of the operators of Functional Reactive Programming (FRP) but with a novel mechanism for reconfiguration that trades expressiveness for improved readability. We present its semantics, describe their encoding into a satisfiability modulo theories solver, and evaluate the performance of its bounded model checking -- First on a toy re-configurable processing pipeline and then a more realistic application. We conclude with a discussion of opportunities for improvement of the model-checking performance and discussion of the interaction of the semantics of functional reactive programming and metric temporal logic.