nach oben

Formal Methods in System Design

Erschienen in:

01.06.2015

Monitoring of temporal first-order properties with aggregations

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

Erschienen in: Formal Methods in System Design | Ausgabe 3/2015

Einloggen

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

search-config

KI-gestützte Suche

Aus

Abstract

In system monitoring, one is often interested in checking properties of aggregated data. Current policy monitoring approaches are limited in the kinds of aggregations they handle. To rectify this, we extend an expressive language, metric first-order temporal logic, with aggregation operators. Our extension is inspired by the aggregation operators common in database query languages like SQL. We provide a monitoring algorithm for this enriched policy specification language. We show that, in comparison to related data processing approaches, our language is better suited for expressing policies, and our monitoring algorithm has competitive performance.

Vorheriger Artikel Synthesising correct concurrent runtime monitors

Nächster Artikel The ins and outs of first-order runtime verification

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 "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

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

Our prototype, the formulas, and the input data are available as an archive at http://sourceforge.net/projects/monpoly/files/fmsd-experiments.tgz.

Abiteboul S, Hull R, Vianu V (1995) Foundations of databases. Addison-Wesley Longman Publishing Co., Inc., BostonMATH

Arasu A, Babcock B, Babu S, Datar M, Ito K, Motwani R, Nishizawa I, Srivastava U, Thomas D, Varma R, Widom J (2003) STREAM: the Stanford stream data manager. IEEE Data Eng Bull 26(1):19–26

Arasu A, Babu S, Widom J (2006) The CQL continuous query language: semantic foundations and query execution. VLDB J 15(2):121–144CrossRef

Barringer H, Goldberg A, Havelund K, Sen K (2004) Rule-based runtime verification. In: Proceedings of the 5th international conference on verification, model checking and abstract interpretation (VMCAI’04). Lecture notes in computer science, vol 2937, pp 44–57

Basin D, Harvan M, Klaedtke F, Zălinescu E (2012) MONPOLY: Monitoring usage-control policies. In: Proceedings of the 2nd international conference on runtime verification (RV’11). Lecture notes in computer science, vol 7186, pp 360–364

Basin D, Harvan M, Klaedtke F, Zălinescu E (2013) Monitoring data usage in distributed systems. IEEE Trans Softw Eng 39(10):1403–1426CrossRef

Basin D, Klaedtke F, Marinovic S, Zălinescu E (2013) Monitoring of temporal first-order properties with aggregations. In: Proceedings of the 4th international conference on runtime verification (RV’13). Lecture notes in computer science, vol 8174, pp 40–58

Basin D, Klaedtke F, Müller S, Pfitzmann B (2008) Runtime monitoring of metric first-order temporal properties. In: Proceedings of the 28th conference on foundations of software technology and theoretical computer science (FSTTCS’08). Leibniz international proceedings in informatics (LIPIcs), vol 2, pp 49–60

Basin D, Klaedtke F, Zălinescu E (2012) Algorithms for monitoring real-time properties. In: Proceedings of the 2nd international conference on runtime verification (RV’11). Lecture notes in computer science, vol 7186, pp 260–275

10.

Bauer A, Goré R, Tiu A (2009) A first-order policy language for history-based transaction monitoring. In: Proceedings of the 6th international colloquium on theoretical aspects of computing (ICTAC’09). Lecture notes in computer science, vol 5684, pp 96–111

11.

Bianculli D, Ghezzi C, Pietro PS (2013) The tale of SOLOIST: A specification language for service compositions interactions. In: Proceedings of the 9th international symposium on formal aspects of component software (FACS’12). Lecture notes in computer science, vol 7684, pp 55–72

12.

Chomicki J (1995) Efficient checking of temporal integrity constraints using bounded history encoding. ACM Trans Database Syst 20(2):149–186CrossRef

13.

Chomicki J, Toman D, Böhlen MH (2001) Querying ATSQL databases with temporal logic. ACM Trans Database Syst 26(2):145–178MATHCrossRef

14.

Colombo C, Gauci A, Pace GJ (2010) LarvaStat: Monitoring of statistical properties. In: Proceedings of the 1st international conference on runtime verification (RV’10). Lecture notes in computer science, vol 6418, pp 480–484

15.

Cranor C, Johnson T, Spataschek O, Shkapenyuk V (2003) Gigascope: A stream database for network applications. In: Proceedings of the 2003 ACM SIGMOD international conference on management of data, pp 647–651

16.

D’Angelo B, Sankaranarayanan S, Sánchez C, Robinson W, Finkbeiner B, Sipma HB, Mehrotra S, Manna Z (2005) LOLA: Runtime monitoring of synchronous systems. In: Proceedings of the 12th international symposium on temporal representation and reasoning (TIME’05), pp 166–174

17.

Finkbeiner B, Sankaranarayanan S, Sipma H (2005) Collecting statistics over runtime executions. Form Methods Syst Des 27(3):253–274MATHCrossRef

18.

Garcia-Molina H, Ullman JD, Widom J (2009) Database systems: the complete book. Pearson Education, Harlow

19.

Hallé S, Villemaire R (2012) Runtime enforcement of web service message contracts with data. IEEE Trans Serv Comput 5(2):192–206CrossRef

20.

Hella L, Libkin L, Nurmonen J, Wong L (2001) Logics with aggregate operators. J ACM 48(4):880–907MATHMathSciNetCrossRef

21.

Koymans R (1990) Specifying real-time properties with metric temporal logic. Real-Time Syst 2(4):255–299CrossRef

22.

Owe O (1993) Partial logics reconsidered: a conservative approach. Form Asp Comput 5(3):208–223MATHMathSciNetCrossRef

23.

PostgreSQL Global Development Group. PostgreSQL, Version 9.1.4, 2012. http://www.postgresql.org/

24.

Sistla AP, Wolfson O (1995) Temporal conditions and integrity constraints in active database systems. In: Proceedings of the 1995 ACM SIGMOD international conference on management of data, pp 269–280

Titel: Monitoring of temporal first-order properties with aggregations
verfasst von: David Basin
Felix Klaedtke
Srdjan Marinovic
Eugen Zălinescu
Publikationsdatum: 01.06.2015
Verlag: Springer US
Erschienen in: Formal Methods in System Design / Ausgabe 3/2015
Print ISSN: 0925-9856
Elektronische ISSN: 1572-8102
DOI: https://doi.org/10.1007/s10703-015-0222-7

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 "Wirtschaft"

Springer Professional "Technik"

Weitere Artikel der Ausgabe 3/2015

The ins and outs of first-order runtime verification

Runtime verification with minimal intrusion through parallelism

Synthesising correct concurrent runtime monitors

Practical interruptible conversations: distributed dynamic verification with multiparty session types and Python

Premium Partner