Adaptive Runtime Verification

Ezio Bartocci (TU Wien)

When: November 13, 1pm

Where: room G2.91b

Abstract

We present Adaptive Runtime Verification (ARV), a new approach to runtime verification in which overhead control, runtime verification with state estimation, and predictive analysis are synergistically combined. Overhead control maintains the overhead of runtime verification at a specified target level, by enabling and disabling monitoring of events for each monitor instance as needed. In ARV, predictive analysis based on a probabilistic model of the monitored system is used to estimate how likely each monitor instance is to violate a given temporal property in the near future, and these criticality levels are fed to the overhead controllers, which allocate a larger fraction of the target overhead to monitor instances with higher criticality, thereby increasing the probability of violation detection. Since overhead control causes the monitor to miss events, we use Runtime Verification with State Estimation (RVSE) to estimate the probability that a property is satisfied by an incompletely monitored run. A key aspect of the ARV framework is a new algorithm for RVSE that performs the calculations offline, dramatically reducing the runtime overhead of RVSE, at the cost of introducing some approximation error. We demonstrate the utility of ARV on a significant case study involving runtime monitoring of concurrency errors in the Linux kernel.

Bio: Ezio Bartocci is currently Assistant Professor (from April 2012) at the Faculty of Informatics, Dependable Systems Group at the Vienna University of Technology. Previously he was a post-doctoral researcher at the Department of Computer Science (Research Scientist - from March 2011) and at the Department of Applied Math and Statistics (Research Associate - from February 2010) of the State University of New York at Stony Brook, working with Prof. James Glimm, Prof. Radu Grosu and Prof. Scott. A. Smolka. He got the Ph.D. (in 2009) in Complex Systems and Information Sciences from the University of Camerino, under the supervision of Prof. Flavio Corradini, Prof. Radu Grosu and Prof. Scott A. Smolka. The primary focus of his research is to develop formal methods, tools and techniques which support the modeling and automated analysis of complex computational systems, including software systems, embedded systems and biological systems.