Collecting Statistics over Runtime Executions

Bernd Finkbeiner, Sriram Sankaranarayanan, Henny Sipma

By collecting statistics over runtime executions of a program we can answer complex queries, such as ``what is the average number of packet retransmissions'' in a communication protocol, or "how often does process P_1 enter the critical section while process P_2 waits" in a mutual exclusion algorithm. We present an extension to linear-time temporal logic that combines the temporal specification with the collection of statistical data. By translating formulas of this language to alternating automata we obtain a simple and efficient query evaluation algorithm. We illustrate our approach with examples and experimental results.

In Runtime Verification, CAV'02 workshop.

Postscript, PDF.

© Henny Sipma /
Last modified: Tue Jul 17 15:29:42 PDT 2001