nach oben

Erschienen in:

2017 | OriginalPaper | Buchkapitel

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

verfasst von : David Basin, Felix Klaedtke, Eugen Zălinescu

Erschienen in: Computer Aided Verification

Verlag: Springer International Publishing

Einloggen

Aktivieren Sie unsere intelligente Suche, um passende Fachinhalte oder Patente zu finden.

search-config

KI-gestützte Suche

Aus

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.

Sie haben noch keine Lizenz? Dann Informieren Sie sich jetzt über unsere Produkte:

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!

Jetzt informieren

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!

Jetzt informieren

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!

Jetzt informieren

Vorheriges Kapitel Runtime Monitoring with Recovery of the SENT Communication Protocol

Nächstes Kapitel Lagrangian Reachabililty

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\).

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.

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\).

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

Barringer, H., Goldberg, A., Havelund, K., Sen, K.: Rule-based runtime verification. In: Steffen, B., Levi, G. (eds.) VMCAI 2004. LNCS, vol. 2937, pp. 44–57. Springer, Heidelberg (2004). doi:10.1007/978-3-540-24622-0_5 CrossRef

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

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

Basin, D., Klaedtke, F., Müller, S., Zălinescu, E.: Monitoring metric first-order temporal properties. J. ACM 62(2), 15 (2015)MathSciNetCrossRefMATH

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)

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

Bauer, A., Falcone, Y.: Decentralised LTL monitoring. In: Giannakopoulou, D., Méry, D. (eds.) FM 2012. LNCS, vol. 7436, pp. 85–100. Springer, Heidelberg (2012). doi:10.1007/978-3-642-32759-9_10 CrossRef

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.

Bauer, A., Leucker, M., Schallhart, C.: Comparing LTL semantics for runtime verification. J. Logic Comput. 20(3), 651–674 (2010)MathSciNetCrossRefMATH

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.

Feng, S., Lohrey, M., Quaas, K.: Path checking for MTL and TPTL over data words. In: Potapov, I. (ed.) DLT 2015. LNCS, vol. 9168, pp. 326–339. Springer, Cham (2015). doi:10.1007/978-3-319-21500-6_26 CrossRef

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.

Maler, O., Nickovic, D.: Monitoring temporal properties of continuous signals. In: Lakhnech, Y., Yovine, S. (eds.) FORMATS/FTRTFT -2004. LNCS, vol. 3253, pp. 152–166. Springer, Heidelberg (2004). doi:10.1007/978-3-540-30206-3_12 CrossRef

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)

Titel: Runtime Verification of Temporal Properties over Out-of-Order Data Streams
verfasst von: David Basin
Felix Klaedtke
Eugen Zălinescu
Verlag: Springer International Publishing
Buch: Computer Aided Verification
Print ISBN: 978-3-319-63386-2

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

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

Springer Professional

Abstract

Bitte loggen Sie sich ein, um Zugang zu Ihrer Lizenz zu erhalten.

Sie haben noch keine Lizenz? Dann Informieren Sie sich jetzt über unsere Produkte:

Springer Professional "Wirtschaft+Technik"

Springer Professional "Technik"

Springer Professional "Wirtschaft"

Premium Partner