Output details
11 - Computer Science and Informatics
University of Oxford
Runtime verification for LTL and TLTL
<07>
This paper pioneers runtime verification of properties given in a formalism dealing with real time properties. In particular, in contrast to earlier approaches, our technique is not only able to deal with clocks describing elapsed time, but also with clocks constraining future events. Although it contains substantial technical proofs, it has been accepted by a top software engineering venue, showing its practical merit.
This 69-page journal paper significantly extends a preliminary 12-page conference version published at FSTTCS’06 that has not been submitted to the RAE 2008. The new contributions of the journals include a proof over 33 pages (Chapter 4), the evaluation based on a prototypical evaluation (Section 2.5 and Appendix A), and a comparison between different LTL semantics (Chapter 3). The proof is the most central result of a series of publications written with Martin Leucker in a collaboration spanning three years.
