Callanan/Grosu/Rai/Smolka,/True/Zadok

Runtime Verification for High-Confidence Systems: A Monte Carlo Approach*

S. Callanan, R. Grosu, A. Rai, S.A. Smolka, M.R. True and E. Zadok

We present a new approach to runtime verification that utilizes classical statistical techniques such as Monte Carlo simulation, hypothesis testing, and confidence interval estimation. Our algorithm, MCM, uses sampling-policy automata to vary its sampling rate dynamically as a function of the current confidence it has in the correctness of the deployed system. We implemented MCM within the Aristotle tool environment, an extensible, GCC-based architecture for instrumenting C programs for the purpose of runtime monitoring. For a case study involving the dynamic allocation and deallocation of objects in the Linux kernel, our experimental results show that Aristotle reduces the runtime overhead due to monitoring, which is initially high when confidence is low, to levels low enough to be acceptable in the long term as confidence in the monitored system grows.

In Proc. of MBT'06, the 2nd Workshop on Model Based Testing, Vienna, Austria, March, 2006.

*This work was partially supported by the NSF Faculty Early Career Development Award CCR01-33583 and the NSF CSR-AES05-09230 Award.