Collecting Statistics over Runtime Executions
Bernd Finkbeiner, Sriram Sankaranarayanan and 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.
Runtime Verification 2002 (RV’02). Electronic Notes in Theoretical Computer Science, Volume 70, Number 4. link (RV 2002).