Runtime verification wtih controllable time predictability and memory utilization

Abstract

The goal of runtime verification is to inspect the well-being of a system by employing a monitor during its execution. Such monitoring imposes costs in terms of resource utilization. Memory usage and predictability of the monitor invocations are among the indicators of the quality of a monitoring solution, especially in the context of embedded systems. In this paper, we propose a novel control-theoretic approach for co-ordinating time predictability and memory utilization in runtime monitoring of real-time embedded systems. In particular, we design a PID controller and four fuzzy controllers with different optimization control objectives. Our approach controls the frequency of when the monitor should be invoked by incorporating a bounded memory buffer that stores events that need to be monitored. The controllers attempt to improve time predictability and maximize memory utilization, while ensuring the soundness of the monitor simultaneously. Unlike the existing approaches based on statis analysis, our approach is highly scalable and well-suited for reactive systems that are required to react to stimuli from the environment in a timely fashion. Our thorough experiments using two case studies (a laser beam stabilizer for aircraft tracking, and a Bluetooth mobile payment system) demonstrate the advantages of using controllers to achieve low variation in the frequency of monitor invocations, while maintaining maximum memory utilization in highly non-linear environments.