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 past-time 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.
Research is supported in part by the National Science Foundation grants CNS-0834524, CNS-0930647, and CNS-1035715.
This is a preview of subscription content, log in via an institution to check access.
Access this chapter
Tax calculation will be finalised at checkout
Purchases are for personal use only
Preview
Unable to display preview. Download preview PDF.
References
Barringer, H., Goldberg, A., Havelund, K., Sen, K.: Program monitoring with LTL in EAGLE. In: Parallel and Distributed Processing Symposium (2004)
Bauer, A., Leucker, M., Schallhart, C.: Comparing LTL Semantics for Runtime Verification. Journal of Logic and Computation (JLC) 20, 651–674 (2010)
Bauer, A., Leucker, M., Schallhart, C.: Runtime verification for LTL and TLTL. ACM Transactions on Software Engineering and Methodology (2011)
Bodden, E.: J-LO—A tool for runtime-checking temporal assertions. Diploma thesis, RWTH Aachen University (November 2005)
Bollig, B., Leucker, M.: Deciding LTL over Mazurkiewicz traces. Data & Knowledge Engineering 44(2), 219–238 (2003)
Clarke, E., Grumberg, O., Peled, D.: Model Checking. MIT Press (1999)
Genest, B., Kuske, D., Muscholl, A., Peled, D.A.: Snapshot Verification. In: Halbwachs, N., Zuck, L.D. (eds.) TACAS 2005. LNCS, vol. 3440, pp. 510–525. Springer, Heidelberg (2005)
Havelund, K., Roşu, G.: Monitoring programs using rewriting. In: International Conference on Automated Software Engineering (2001)
Havelund, K., Roşu, G.: Synthesizing Monitors for Safety Properties. In: Katoen, J.-P., Stevens, P. (eds.) TACAS 2002. LNCS, vol. 2280, pp. 342–356. Springer, Heidelberg (2002)
Havelund, K., Roşu, G.: Efficient monitoring of safety properties. Int. J. Softw. Tools Technol. Transf. 6(2), 158–173 (2004)
Kleene, S.C.: Introduction to Metamathematics. D. Van Nostrand (1950)
Lee, I., Kannan, S., Kim, M., Sokolsky, O., Viswanathan, M.: Runtime assurance based on formal specifications. In: PDPTA 1999, pp. 279–287 (1999)
Manna, Z., Pnueli, A.: The temporal logic of reactive and concurrent systems: specification, vol. 1. Springer, Heidelberg (1992)
Mazurkiewicz, A.: Concurrent program schemes and their interpretations. Tech. rep., DAIMI Rep. PB 78, Aarhus University (1977)
Pnueli, A.: The temporal logic of programs. In: 18th Annual Symposium on Foundations of Computer Science, pp. 46–57. IEEE (1977)
Rozier, K., Vardi, M.: LTL Satisfiability Checking. In: Bošnački, D., Edelkamp, S. (eds.) SPIN 2007. LNCS, vol. 4595, pp. 149–167. Springer, Heidelberg (2007)
SAnToS Lab, Kansas State University: Property pattern mappings for LTL, http://patterns.projects.cis.ksu.edu/documentation/patterns/ltl.shtml
Spees, W.S.: Functional Requirement for LDR Component. Center for Devices and Radiological Health, FDA (2010)
Tauriainen, H., Heljanko, K.: Testing LTL formula translation into Büchi automata. STTT 4(1), 57–70 (2002)
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2012 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Wang, S., Ayoub, A., Sokolsky, O., Lee, I. (2012). Runtime Verification of Traces under Recording Uncertainty. In: Khurshid, S., Sen, K. (eds) Runtime Verification. RV 2011. Lecture Notes in Computer Science, vol 7186. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-642-29860-8_35
Download citation
DOI: https://doi.org/10.1007/978-3-642-29860-8_35
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-642-29859-2
Online ISBN: 978-3-642-29860-8
eBook Packages: Computer ScienceComputer Science (R0)