Beyond single traces : implementing multiple execution monitoring in DetectEr

Abstract

Runtime verification (RV) has emerged as a crucial technique for ensuring software correctness by monitoring system execution against formally specified properties. However, traditional RV approaches are limited to analyzing single execution traces, restricting their ability to verify properties that require evidence from multiple system runs, particularly in branching-time systems. This project extends DetectEr, an open-source runtime verification tool for actor-based systems, to support multiple execution monitoring. The extension enables verification of safety properties expressed in sHML∨ Det, an enhanced specification language that incorporates disjunctive operators beyond the original Safety Hennessy-Milner Logic (sHML). The implementation addresses three key challenges: adapting the theoretical framework to handle first-order events with data values, developing a robust history aggregation mechanism using Erlang Term Storage tables with trace normalisation, and implementing a breadth-first search algorithm for the history analysis proof system. The approach successfully demonstrates the practical feasibility of multiple execution monitoring through evaluation using a calculator server case study. The results show that the extended framework maintains backward compatibility with existing DetectEr functionality while enabling verification of previously unmonitorable properties, such as implication-based conditions requiring evidence across multiple execution traces. This work contributes to the runtime verification field by demonstrating that multiple execution monitoring can be effectively integrated into existing RV frameworks, expanding their verification capabilities.