Skip to main content
Disciplines
Automotive Business IT + Informatics Construction + Real Estate Electrical Engineering + Electronics Energy + Sustainability Insurance + Risk Finance + Banking Management + Leadership Marketing + Sales Mechanical Engineering + Materials
Events
DE
EN
Books
Journals
Topic Page
Marketing
Start single access now
Access for companies
EXTENDED SEARCH
Log in
Top
Published in:
Safety Verification of Deep Neural Networks Read chapter Read first chapter

2017 | OriginalPaper | Chapter

Runtime Verification of Temporal Properties over Out-of-Order Data Streams

Authors : David Basin, Felix Klaedtke, Eugen Zălinescu

Published in: Computer Aided Verification

Publisher: Springer International Publishing

Log in

Activate our intelligent search to find suitable subject content or patents.

search-config
loading …

Abstract

We present a monitoring approach for verifying systems at runtime. Our approach targets systems whose components communicate with the monitors over unreliable channels, where messages can be delayed or lost. In contrast to prior works, whose property specification languages are limited to propositional temporal logics, our approach handles an extension of the real-time logic MTL with freeze quantifiers for reasoning about data values. We present its underlying theory based on a new three-valued semantics that is well suited to soundly and completely reason online about event streams in the presence of message delay or loss. We also evaluate our approach experimentally. Our prototype implementation processes hundreds of events per second in settings where messages are received out of order.

Dont have a licence yet? Then find out more about our products and how to get one now:

Springer Professional "Wirtschaft+Technik"

Online-Abonnement

Mit Springer Professional "Wirtschaft+Technik" erhalten Sie Zugriff auf:

  • über 102.000 Bücher
  • über 537 Zeitschriften

aus folgenden Fachgebieten:

  • Automobil + Motoren
  • Bauwesen + Immobilien
  • Business IT + Informatik
  • Elektrotechnik + Elektronik
  • Energie + Nachhaltigkeit
  • Finance + Banking
  • Management + Führung
  • Marketing + Vertrieb
  • Maschinenbau + Werkstoffe
  • Versicherung + Risiko

Jetzt Wissensvorsprung sichern!

inform now

Springer Professional "Technik"

Online-Abonnement

Mit Springer Professional "Technik" erhalten Sie Zugriff auf:

  • über 67.000 Bücher
  • über 390 Zeitschriften

aus folgenden Fachgebieten:

  • Automobil + Motoren
  • Bauwesen + Immobilien
  • Business IT + Informatik
  • Elektrotechnik + Elektronik
  • Energie + Nachhaltigkeit
  • Maschinenbau + Werkstoffe




 

Jetzt Wissensvorsprung sichern!

inform now

Springer Professional "Wirtschaft"

Online-Abonnement

Mit Springer Professional "Wirtschaft" erhalten Sie Zugriff auf:

  • über 67.000 Bücher
  • über 340 Zeitschriften

aus folgenden Fachgebieten:

  • Bauwesen + Immobilien
  • Business IT + Informatik
  • Finance + Banking
  • Management + Führung
  • Marketing + Vertrieb
  • Versicherung + Risiko




Jetzt Wissensvorsprung sichern!

inform now
previous chapter Runtime Monitoring with Recovery of the SENT Communication Protocol
next chapter Lagrangian Reachabililty
Footnotes
1
We assume here that the timed words are over the alphabet \(\varSigma \) that consists of the pairs \((\sigma ,\varrho )\), where (i) \(\sigma \) is a total function over P with \(\sigma (p)\subseteq D^{\iota (p)}\) for \(p\in P\), and (ii) \(\varrho \) is a total function over R with \(\varrho (r)\in D\) for \(r\in R\).
 
2
We consider here that the formulas defining the semantics are first simplified. E.g., assuming that https://static-content.springer.com/image/chp%3A10.1007%2F978-3-319-63387-9_18/454766_1_En_18_IEq410_HTML.gif is reached, \(k\in pos (w_i)\), and \(k\ge j\), if \({\mathrm {tc}_{w_i,I}(k,j)=\mathsf {f}}\), then https://static-content.springer.com/image/chp%3A10.1007%2F978-3-319-63387-9_18/454766_1_En_18_IEq414_HTML.gif is not reached, otherwise (i.e. \(\mathrm {tc}_{w_i,I}(k,j)\ne \mathsf {f}\)) it is reached.
 
3
For instance, for the formula https://static-content.springer.com/image/chp%3A10.1007%2F978-3-319-63387-9_18/454766_1_En_18_IEq622_HTML.gif , if p does not hold at time point i with timestamp \(\tau \), then our prototype outputs the corresponding verdict directly after processing the time point i, whereas MONPOLY reports this violation at the first time point with a timestamp larger than \(\tau +3\).
 
Literature
1.
Alur, R., Henzinger, T.A.: Logics and models of real time: a survey. In: Bakker, J.W., Huizing, C., Roever, W.P., Rozenberg, G. (eds.) REX 1991. LNCS, vol. 600, pp. 74–106. Springer, Heidelberg (1992). doi:10.​1007/​BFb0031988 CrossRef
2.
3.
Basin, D., Harvan, M., Klaedtke, F., Zălinescu, E.: MONPOLY: monitoring usage-control policies. In: Khurshid, S., Sen, K. (eds.) RV 2011. LNCS, vol. 7186, pp. 360–364. Springer, Heidelberg (2012). doi:10.​1007/​978-3-642-29860-8_​27 CrossRef
4.
Basin, D., Klaedtke, F., Marinovic, S., Zălinescu, E.: Monitoring compliance policies over incomplete and disagreeing logs. In: Qadeer, S., Tasiran, S. (eds.) RV 2012. LNCS, vol. 7687, pp. 151–167. Springer, Heidelberg (2013). doi:10.​1007/​978-3-642-35632-2_​17 CrossRef
5.
6.
Basin, D., Klaedtke, F., Zălinescu, E.: Failure-aware runtime verification of distributed systems. In: Proceedings of 35th International Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS), Leibniz International Proceedings in Informatics (LIPIcs), vol. 45, pp. 590–603. Schloss Dagstuhl - Leibniz Center for Informatics (2015)
7.
Basin, D., Klaedtke, F., Zălinescu, E.: Runtime verification of temporal properties over out-of-order data streams (2017). Full version of this paper: arXiv.​org
8.
9.
Bauer, A., Küster, J., Vegliach, G.: The ins and outs of first-order runtime verification. Form. Methods Syst. Des. 46(3), 286–316 (2015)CrossRefMATH
10.
11.
Bauer, A., Leucker, M., Schallhart, C.: Runtime verification for LTL and TLTL. ACM Trans. Softw. Eng. Meth. 20(4), 14 (2011)CrossRef
12.
Colombo, C., Falcone, Y.: Organising LTL monitors over distributed systems with a global clock. Form. Methods Syst. Des. 49(1), 109–158 (2016)CrossRef
13.
14.
Garg, D., Jia, L., Datta, A.: Policy auditing over incomplete logs: theory, implementation and applications. In: Proceedings of 18th ACM Conference on Computer and Communications Security (CCS), pp. 151–162. ACM Press (2011)
15.
Goidefroid, P., Piterman, N.: LTL generalized model checking revisited. Int. J. Softw. Tools Technol. Trans. 13(6), 571–584 (2011)CrossRef
16.
Henzinger, T.A.: Half-order modal logic: how to prove real-time properties. In: Proceedings of 9th Annual ACM Symposium on Principles of Distributed Computing (PODC), pp. 281–296. ACM Press (1990)
17.
Koymans, R.: Specifying real-time properties with metric temporal logic. Real-Time Syst. 2(4), 255–299 (1990)CrossRef
18.
19.
Meredith, P.O., Jin, D., Griffith, D., Chen, F., Rou, G.: An overview of the MOP runtime verification framework. Int. J. Softw. Tools Technol. Trans. 14(3), 249–289 (2012)CrossRef
20.
Mostafa, M., Bonakdarbour, B.: Decentralized runtime verification of LTL specifications in distributed systems. In: Proceedings of 29th IEEE International Parallel and Distributed Processing Symposium (IPDPS). IEEE Computer Society (2015)
21.
Ouaknine, J., Worrell, J.: On metric temporal logic and faulty turing machines. In: Aceto, L., Ingólfsdóttir, A. (eds.) FoSSaCS 2006. LNCS, vol. 3921, pp. 217–230. Springer, Heidelberg (2006). doi:10.​1007/​11690634_​15 CrossRef
22.
Sen, K., Vardhan, A., Agha, G., Rou, G.: Efficient decentralized monitoring of safety in distributed systems. In: Proceedings of 26th International Conference on Software Engineering (ICSE), pp. 418–427. IEEE Computer Society (2004)
Metadata
Title
Runtime Verification of Temporal Properties over Out-of-Order Data Streams
Authors
David Basin
Felix Klaedtke
Eugen Zălinescu
Copyright Year
2017
Book
Computer Aided Verification

Print ISBN: 978-3-319-63386-2

Electronic ISBN: 978-3-319-63387-9

Copyright Year: 2017

DOI
https://doi.org/10.1007/978-3-319-63387-9_18

Premium Partner

    Image Credits