Runtime verification of timed regular expressions in Larva

Abstract

Runtime verification (RV) is based on the use of monitors to verify whether a computer program behaves as expected at runtime. One of the critical factors of this technique is the overhead that the monitoring adds to the system under verification. A program's expected behaviour is defined by a specification typically expressed using some formal logic. This selected logic and the approach used to adapt the formalism to runtime verification has a direct influence on the degree of overhead produced by the resultant monitor, which must be minimized as much as possible while conserving the expressive power of the logic. Using the Larva RV tool and its automaton-based DATEs language as an RV foundation, this project investigates the potential of timed regular expressions (TREs) as a specification language. Two approaches by which TREs can be adapted to RV are presented and compared in terms of the overhead that they produce. These include an approach based on timed derivatives, where the original TRE changes shape in response to events, and an approach based on explicit state exploration, involving the conversion of TREs to timed automata, which are then translated into Larva's DATEs language. A major contribution of this project is a replication technique which allows certain timed automation non-determinism to be handled using deterministic RV tools, such as Larva. To evaluate the two implemented approaches, five properties were specified for a real- world FTP server use case, which was then monitored according to these properties to measure the memory and CPU overhead added to the FTP server. Through a set of experiments, we find that both approaches produce significant overhead, but the timed derivatives approach outperforms the timed automata approach both in terms of overhead and in terms of the general complexity of the approach.