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.
Formal Methods in System Design. Volume 27, Issue 3, Nov 2005, Pages 253 – 274 (FMSD 2005).
Journal version of [FSS02].