Collecting Statistics Over Runtime Executions |
| |
Authors: | Bernd Finkbeiner Sriram Sankaranarayanan Henny B Sipma |
| |
Affiliation: | 1.Max-Planck-Institut für Informatik,Saarbrücken,Germany;2.Fachrichtung Informatik,Universit?t des Saarlandes,Saarbrücken,Germany;3.Computer Science Department,Stanford University,Stanford,USA |
| |
Abstract: | We present an extension to linear-time temporal logic (LTL) that combines the temporal specification with the collection of
statistical data. By collecting statistics over runtime executions of a program we can answer complex queries, such as “what
is the average number of packet transmissions' in a communication protocol, or “how often does a particular process enter
the critical section while another process remains waiting' in a mutual exclusion algorithm. To decouple the evaluation strategy
of the queries from the definition of the temporal operators, we introduce algebraic alternating automata as an automata-based
intermediate representation. Algebraic alternating automata are an extension of alternating automata that produce a value
instead of acceptance or rejection for each trace. Based on the translation of the formulas from the query language to algebraic
alternating automata, we obtain a simple and efficient query evaluation algorithm. The approach is illustrated with examples
and experimental results. |
| |
Keywords: | program profiling runtime verification specification languages runtime monitoring temporal logic |
本文献已被 SpringerLink 等数据库收录! |
|