Skip to main content
Article
Runtime Verification of Traces Under Recording Uncertainty
Lecture Notes in Computer Science: Runtime Verification
  • Shaohui Wang, University of Pennsylvania
  • Anaheed Ayoub, University of Pennsylvania
  • Oleg Sokolsky, University of Pennsylvania
  • Insup Lee, University of Pennsylvania
Date of this Version
9-1-2011
Document Type
Conference Paper
Comments
Second International Conference, RV 2011, San Francisco, CA, USA, September 27-30, 2011.
Conference site: http://rv2011.eecs.berkeley.edu/Home.html

Abstract

We present an on-line algorithm for the runtime checking of temporal properties, expressed as past-time Linear Temporal Logic (LTL) over the traces of observations recorded by a "black box"-like device. The recorder captures the observed values but not the precise time of their occurrences, and precise truth evaluation of a temporal logic formula cannot always be obtained. In order to handle this uncertainty, the checking algorithm is based on a three-valued semantics for pasttime LTL defined in this paper. In addition to the algorithm, the paper presents results of an evaluation that aimed to study the effects of the recording uncertainty on different kinds of temporal logic properties.

DOI
10.1007/978-3-642-29860-8_35
Copyright/Permission Statement
The final publication is available at Springer via http://dx.doi.org/10.1007/978-3-642-29860-8_35
Citation Information
Shaohui Wang, Anaheed Ayoub, Oleg Sokolsky and Insup Lee. "Runtime Verification of Traces Under Recording Uncertainty" Lecture Notes in Computer Science: Runtime Verification Vol. 7186 (2011) p. 442 - 456
Available at: http://works.bepress.com/sokolsky/90/