Runtime monitoring for asynchronous reactive components

Abstract

Modern software is built on reactive principles, where systems are responsive, resilient, elastic, and message-driven. Despite the benefits they engender, these aspects make the correctness of reactive systems in terms of their expected behaviour hard to ascertain statically. This thesis investigates how the correctness of reactive systems can be ascertained dynamically at runtime. It considers a lightweight monitoring technique, called runtime verification, that circumvents the issues associated with traditional pre-deployment techniques. One major challenge of runtime verification lies in choosing a monitoring approach that does not impinge on the reactive aspects of the system under scrutiny. Such a goal is met only if the monitoring system is itself reactive. We propose a novel monitoring approach grounded on this precept. It treats the system as a black box, instrumenting monitors dynamically and in an asynchronous fashion, which is in tune with the requirements of reactive architectures. Our development approach is systematic, permitting us to directly map the constituent parts of our formal model to implementable modules. This gives assurances that the results obtained in the theory are preserved in the implementation.

The first part of the thesis builds on established theoretical results. It lifts these results to a first-order setting to accommodate scenarios where systems manipulate data. We define an asynchronous instrumentation relation that decouples the operation of the system from that of its monitors. This definition forms the basis of our decentralised outline monitoring algorithm presented in the second part of the thesis. Our algorithm employs a tracing infrastructure to collect trace events as the system executes and uses key events as cues to instrument new monitors or terminate redundant ones dynamically. It accounts for the interleaving of events that arises from the asynchronous execution of the system and monitors, guaranteeing that events are analysed by monitors in the correct sequence and without gaps.

Part three develops a runtime verification benchmarking framework that is tailored for reactive systems. The framework can generate models that faithfully capture the realistic behaviour of master-worker systems under typical load characteristics. Our tool collects different performance metrics suited to reactive applications, to give a multi-faceted depiction of the overhead induced by runtime monitoring tools. Part four of this thesis embarks on an extensive evaluation of our decentralised outline monitoring algorithm using the benchmarking tool developed in part three. The algorithm is compared against our implementation of inline and centralised monitoring---two prevalent methods used in state-of-the-art runtime verification tools. Apart from demonstrating that our monitoring algorithm is reactive, the experiments we conduct testify that it induces acceptable overhead that, in typical cases, is comparable to that of inlining. These results also confirm that centralised monitoring is prone to scalability issues, poor performance, and failure, making it generally inapplicable to reactive system settings. We are unaware of other comprehensive empirical runtime verification studies such as ours that compare decentralised, centralised, and inline monitoring.