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 January 2005
Contact Data Privacy Policy Imprint
Home People Publications
More