Skip to main content
Fachgebiete
Automobil + Motoren Bauwesen + Immobilien Business IT + Informatik Elektrotechnik + Elektronik Energie + Nachhaltigkeit Finance + Banking Management + Führung Marketing + Vertrieb Maschinenbau + Werkstoffe Versicherung + Risiko
DE
EN
Bücher
Zeitschriften
Themenseiten
Organisationspsychologie Projektmanagement Marketing Smart Manufacturing
Weitere Formate
Podcasts Webinare Technik Webinare Wirtschaft Kongresse Veranstaltungskalender Awards
Jetzt Einzelzugang starten
Zugang für Unternehmen
Referenzkunden
SLX-Digitalkonferenz: Zukunftswerkstatt 2024

Mehr Umsatz mit Top-Kontakten

Am 7. Mai erfahren Sie, wie Vertriebsteams Leadgenerierung, Leadnurturing und Leadstrategien effizient steuern können.
Erweiterte Suche
Anmelden
nach oben
Formal Methods in System Design
Erschienen in: Formal Methods in System Design 1/2018

27.02.2018

Inferring event stream abstractions

verfasst von: Sean Kauffman, Klaus Havelund, Rajeev Joshi, Sebastian Fischmeister

Erschienen in: Formal Methods in System Design | Ausgabe 1/2018

Einloggen

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

search-config
loading …

Abstract

We propose a formalism for specifying event stream abstractions for use in spacecraft telemetry processing. Our work is motivated by the need to quickly process streams with millions of events generated e.g. by the Curiosity rover on Mars. The approach builds a hierarchy of event abstractions for telemetry visualization and querying to aid human comprehension. Such abstractions can also be used as input to other runtime verification tools. Our notation is inspired by Allen’s Temporal Logic, and provides a rule-based declarative way to express event abstractions. We present an algorithm for applying specifications to an event stream and explore modifications to improve the algorithm’s asymptotic complexity. The system is implemented in both Scala and C, with the specification language implemented as internal as well as external DSLs. We illustrate the solution with several examples, a performance evaluation, and a real telemetry analysis scenario.
Vorheriger Artikel Wireless protocol validation under uncertainty
Nächster Artikel Quantitative monitoring of STL with edit distance

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
Fußnoten
1
Visualization of information is e.g. at JPL considered an important approach to aid humans in daily spacecraft operations.
 
2
\(\mathcal{V}\) can be any set of values that are part of monitored events.
 
3
The trace is artificially constructed to have no resemblance to real artifacts.
 
4
A limited form of disjunction is also allowed but not described here.
 
5
Time stamps have no specified units and their interpretation depends on the specification.
 
6
The GUI was designed and implemented by Nathaniel Guy (JPL).
 
7
Note that the eDSL uses https://static-content.springer.com/image/art%3A10.1007%2Fs10703-018-0317-z/MediaObjects/10703_2018_317_Figt_HTML.gif to denote the start time of an interval, in contrast to the notation in Sect. 4 where it was referred to as start (time).
 
8
The eDSL supports unary rules but we will avoid describing them here as they represent a special case.
 
Literatur
1.
Albarghouthi A, Baier JA, McIlraith SA (2009) On the use of planning technology for verification. In: Proceedings of the ICAPS workshop on verification & validation of planning & scheduling systems (VVPS), Citeseer
2.
Allen JF (1983) Maintaining knowledge about temporal intervals. Commun ACM 26(11):832–843CrossRefMATH
3.
Allen JF (1984) Towards a general theory of action and time. Artif Intell 23(2):123–154CrossRefMATH
4.
Alur R, Fisman D, Raghothaman M (2016) Regular programming for quantitative properties of data streams. In: Programming languages and systems—25th European symposium on programming, ESOP 2016, Eindhoven, The Netherlands. Springer, LNCS, vol 9632, pp 15–40
5.
Arasu A, Babu S, Widom J (2006) The CQL continuous query language: semantic foundations and query execution. Int J Very Large Data Bases 15(2):121–142CrossRef
6.
Barringer H, Havelund K (2011) TraceContract: a scala DSL for trace analysis. In: Proceedings of the 17th international symposium on formal methods (FM’11). Springer, LNCS, vol 6664, pp 57–72
7.
Barringer H, Goldberg A, Havelund K, Sen K (2004) Rule-based runtime verification. In: International conference on verification, model checking, and abstract interpretation (VMCAI), vol 2937, pp 44–57
8.
Barringer H, Rydeheard D, Havelund K (2008) Rule systems for run-time monitoring: from Eagle to RuleR. J Log Comput 20(3):675–706MathSciNetCrossRefMATH
9.
Barringer H, Falcone Y, Havelund K, Reger G, Rydeheard D (2012) Quantified event automata: towards expressive and efficient runtime monitors. In: Proceedings of the 18th international symposium on formal methods (FM’12). Springer, pp 68–84. https://​doi.​org/​10.​1007/​978-3-642-32759-9_​9
10.
Basin D, Harvan M, Klaedtke F, Zălinescu E (2011) MONPOLY: monitoring usage–control policies. In: 2nd international conference on runtime verification (RV’11). Springer, LNCS, vol 7186, pp 360–364
11.
12.
Bauer A, Leucker M, Schallhart C (2007) The good, the bad, and the ugly, but how ugly is ugly? In: 7th International workshop on runtime verification (RV’07). Springer, LNCS, vol 4839, pp 126–138
13.
Bauer A, Leucker M, Schallhart C (2011) Runtime verification for LTL and TLTL. ACM Trans Softw Eng Methodol (TOSEM) 20(4):14CrossRef
14.
Butler RW, Siminiceanu RI, Muno C (2007) The ANMLite language and logic for specifying planning problems. Report 215088:23681–2199
15.
Chen F, Roşu G (2007) MOP: an efficient and generic runtime verification framework. In: ACM SIGPLAN notices. ACM, vol 42, pp 569–588
16.
17.
Colombo C, Pace GJ, Schneider G (2009) Larva—safer monitoring of real-time java programs (tool paper). In: Proceedings of the 2009 seventh IEEE international conference on software engineering and formal methods. IEEE Computer Society, Washington, DC, USA, SEFM ’09, pp 33–37. https://​doi.​org/​10.​1109/​SEFM.​2009.​13
18.
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. ACM, pp 647–651
19.
Cugola G, Margara A (2012) Processing flows of information: from data stream to complex event processing. ACM Comput Surv (CSUR) 44(3):15CrossRef
20.
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. IEEE Computer Society, pp 166–174
21.
Decker N, Leucker M, Thoma D (2013) jUnitRV—adding runtime verification to jUnit. In: Brat G, Rungta N, Venet A (eds) NASA formal methods, 5th international symposium, NFM 2013, Moffett Field, CA, USA, May 14–16, 2013. Proceedings. Springer, Lecture Notes in Computer Science, vol 7871, pp 459–464. https://​doi.​org/​10.​1007/​978-3-642-38088-4_​34
22.
23.
Dillon LK, Kutty G, Moser LE, Melliar-Smith PM, Ramakrishna YS (1994) A graphical interval logic for specifying concurrent systems. ACM Trans Softw Eng Methodol 3:131–165CrossRefMATH
24.
Doorenbos RB (1995) Production matching for large learning systems. Ph.D. thesis, Carnegie Mellon University, Pittsburgh, PA, USA
25.
26.
Eckert M, Bry F (2009) Complex event processing (CEP). Informatik-Spektrum 32(2):163–167CrossRef
27.
Ernst MD, Perkins JH, Guo PJ, McCamant S, Pacheco C, Tschantz MS, Xiao C (2007) The Daikon system for dynamic detection of likely invariants. Sci Comput Progr 69(1):35–45MathSciNetCrossRefMATH
28.
29.
Finkbeiner B, Sankaranarayanan S, Sipma H (2005) Collecting statistics over runtime executions. Form Methods Syst Des 27(3):253–274CrossRefMATH
30.
Forgy C (1982) Rete: a fast algorithm for the many pattern/many object pattern match problem. Artif Intell 19:17–37CrossRef
31.
Goubault-Larrecq J, Olivain J (2008) A smell of ORCHIDS. In: Proceedings of the 8th international workshop on runtime verification (RV’08). Springer, LNCS, vol 5289, pp 1–20
32.
Hallé S (2016) When RV, Meets CEP. In: Runtime verification: Proceedings of 16th international conference, RV 2016, Madrid, Spain, September 23–30, 2016. Springer, pp 68–91
33.
Hallé S, Gaboury S, Bouchard B (2016) Activity recognition through complex event processing: first findings. In: AAAI workshop: artificial intelligence applied to assistive technologies and smart environments
34.
Hansen MR, Van Hung D (2007) A theory of duration calculus with application. In: Domain modeling and the duration calculus, LNCS, vol 4710. Springer, pp 119–176
35.
Havelund K (2015) Rule-based runtime verification revisited. Int J Softw Tools Technol Transf 17(2):143–170CrossRef
36.
Havelund K, Joshi R (2014) Comprehension of spacecraft telemetry using hierarchical specifications of behavior. In: Merz S, Pang J (eds) Formal methods and software engineering: 16th international conference on formal engineering methods, ICFEM 2014, Luxembourg, November 3–5, 2014. Proceedings. Springer International Publishing, LNCS, vol 8829, pp 187–202
37.
Havelund K, Joshi R (2015) Experience with rule-based analysis of spacecraft logs. In: Artho C, Ölveczky CP (eds) Formal techniques for safety-critical systems: third international workshop (FTSCS 2014), November 2014, Luxembourg. Springer International Publishing, Communications in Computer and Information Science, vol 476, pp 1–16
38.
Havelund K, Peled D, Ulus D (2017) First order temporal logic monitoring with BDDs. 17th Conference on formal methods in computer-aided design (FMCAD 2017), 2–6 October, Austria. IEEE Computer Society, Vienna, pp 116–123
39.
40.
Kauffman S, Havelund K, Joshi R (2016) nfer—a notation and system for inferring event stream abstractions. In: Falcone Y, Sánchez C (eds) Runtime verification: 16th international conference, RV 2016, Madrid, Spain, September 23–30, 2016, Proceedings. Springer, LNCS, vol 10012, pp 235–250
41.
42.
Kreps J, Narkhede N, Rao J (2011) Kafka: a distributed messaging system for log processing. In: Proceedings of the 6th international workshop on networking meets databases (NetDB’11). ACM, pp 1–7
43.
Legay A, Delahaye B, Bensalem S (2010) Statistical model checking: an overview. In: 1st international conference on runtime verification (RV’10). Springer, LNCS, vol 6418
44.
45.
Luckham D (2002) The power of events: an introduction to complex event processing in distributed enterprise systems. Addison-Wesley, Boston
46.
Mcdermott D, Ghallab M, Howe A, Knoblock C, Ram A, Veloso M, Weld D, Wilkins D (1998) PDDL—the planning domain definition language. Tech. rep., CVC TR-98-003/DCS TR-1165, Yale Center for Computational Vision and Control
47.
48.
Moszkowski BC (1985) A temporal logic for multilevel reasoning about hardware. IEEE Comput 18:10–19CrossRef
49.
Narayan A, Kauffman S, Morgan J, Tchamgoue GM, Joshi Y, Hobbs C, Fischmeister S (2017) System call logs with natural random faults: experimental design and application. In: SELSE-13: the 13th workshop on silicon errors in logic, system effects, Boston, MA, USA
50.
Navabpour S, Joshi Y, Wu W, Berkovich S, Medhat R, Bonakdarpour B, Fischmeister S (2013) RiTHM: a tool for enabling time-triggered runtime verification for C programs. In: Proceedings of the 2013 9th joint meeting on foundations of software engineering. ACM, pp 603–606
51.
QNX (1997) QNX operating system: system architecture. QNX Software Systems Ltd, Ontario
52.
R Development Core Team (2008) R: A Language and Environment for Statistical Computing. R Foundation for Statistical Computing, Vienna, Austria. ISBN: 3-900051-07-0. http://​www.​R-project.​org
53.
Reger G (2014) Automata based monitoring and mining of execution traces. Ph.D. thesis, University of Manchester
54.
Reger G, Cruz HC, Rydeheard D (2015) MarQ: monitoring at runtime with QEA. In: Proceedings of the 21st international conference on tools and algorithms for the construction and analysis of systems (TACAS’15)
55.
Rosu G, Bensalem S (2006) Allen linear (interval) temporal logic—translation to LTL and monitor synthesis. In: 18th international conference on computer aided verification (CAV’06). Springer, LNCS, vol 4144, pp 263–277
56.
Siminiceanu R, Butler RW, Muñoz CA (2009) Experimental evaluation of a planning language suitable for formal verification. In: 5th international workshop on model checking and artificial intelligence (MoChArt’08), LNCS, vol 5348. Springer, pp 132–146
57.
Metadaten
Titel
Inferring event stream abstractions
verfasst von
Sean Kauffman
Klaus Havelund
Rajeev Joshi
Sebastian Fischmeister
Publikationsdatum
27.02.2018
Verlag
Springer US
Erschienen in
Formal Methods in System Design / Ausgabe 1/2018
Print ISSN: 0925-9856
Elektronische ISSN: 1572-8102
DOI
https://doi.org/10.1007/s10703-018-0317-z

Weitere Artikel der Ausgabe 1/2018

Formal Methods in System Design 1/2018 Zur Ausgabe

EditorialNotes

Introduction to the special issue on runtime verification

OriginalPaper

Quantitative monitoring of STL with edit distance

OriginalPaper

Non-intrusive runtime monitoring through power consumption to enforce safety and security properties in embedded systems

OriginalPaper

Wireless protocol validation under uncertainty

OriginalPaper

On the complexity of monitoring Orchids signatures, and recurrence equations

OriginalPaper

Finite-trace linear temporal logic: coinductive completeness