Speaker
Deepak Kumar
Title
Runtime Verification with 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 work, we propose a novel control-theoretic approach for coordinating 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 di 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 static 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 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.