Monitoring incomplete traces navigating uncertainty

Abstract

As software systems scale in size and complexity, manual code reviews become increasingly more resource intensive, underscoring the critical need for reliable Runtime Verification (RV) techniques. Traditional RV approaches assume complete access to error-free execution trace, an assumption that is untenable in real-world scenarios. This work address the challenges of monitoring such incomplete traces by proposing a novel methodology that synthesises sound and modular runtime monitors. Building upon detectEr, our monitors are able to handle non-consecutive missing events in observed traces. We demonstrate a scalable and sound framework that facilitates verdict generation through deterministic state inference, enabling monitors to achieve greater completeness on data restricted traces. The methodology combines a theoretically rigorous approach with practicality in mind, utilising an automaton-guided state regeneration technique for state inference. The findings from our evaluation demonstrate the efficacy of the proposed solution across several examples. The modular monitors are capable of navigating through data-restricted traces and producing sound, irrevocable verdicts. This thesis contributes to the field of RV by establishing a sound foundation for the deterministic inference of missing events in incomplete traces, and also provides a framework that increases the applicability of monitors by taking a compositional approach to monitor synthesis. By bridging a gap that is often overlooked in this field,such a solution is required, especially in recent years, as systems are becoming exponentially more complex.