Project

Back to overview

Big Data Monitoring

Applicant Basin David
Number 167162
Funding scheme NRP 75 Big Data
Research institution Information security group Department of Computer Science ETH Zürich
Institution of higher education ETH Zurich - ETHZ
Main discipline Information Technology
Start/End 01.01.2017 - 31.12.2020
Approved amount 470'108.00
Show all

All Disciplines (2)

Discipline
Information Technology
Mathematics

Keywords (6)

runtime verification; large-scale monitoring; temporal logic; data stream management system; stream reasoning; event stream

Lay Summary (German)

Lead
Die Arbeitsabläufe vieler Behörden und Unternehmen sind stark reglementiert. In der Praxis ist es oft schwierig festzustellen, ob gegebene Regeln tatsächlich eingehalten werden. Wir entwickeln Algorithmen zur automatisierten Regelüberprüfung, die mit grossen Datenmengen umgehen können.Wir entwickeln und implementieren effiziente, parallelisierte Algorithmen, die Daten in einer dynamischen Umgebung auf die Einhaltung von Regeln prüfen können. Als Eingabe erhalten diese Algorithmen einen in Echtzeit ankommenden Datenstrom sowie die zu prüfenden Regeln. Die Regeln werden dabei in einer festgelegten Eingabesprache formuliert. Diese muss ihren Nutzern erlauben, zeitliche und inhaltliche Zusammenhänge zwischen unterschiedlichen Datenpunkten auf einfache und intuitive Weise auszudrücken. Bei Regelverstössen erfolgt eine kompakte Ausgabe der für den Verstoss verantwortlichen Daten.
Lay summary

Regelkonformität oder Compliance ist eine wichtige Aufgabe, der Unternehmen ganze Abteilungen widmen. Diese Abteilungen müssen mitunter komplexe Abläufe anhand von Ereignisprotokollen oder Logdateien von beträchtlichem Umfang schnell und zuverlässig auf Einhaltung gegebener Regeln prüfen. Eine typische Regel für eine Bank könnte lauten: Kein Kunde darf mehr als 5000 Franken pro Woche abheben. Die Identifizierung einzelner Verstösse ist von grossem Wert.

Wir entwickeln Algorithmen, die kontinuierlich ankommende Daten auf Regelverstösse überprüfen. Je komplexer die Regel, desto grösser ist die Herausforderung, sie auf enormen Datenmengen effizient zu prüfen. Die Ausdrucksstärke der Eingabesprache beeinflusst die mögliche Komplexität der Regeln und damit auch die Effizienz der Algorithmen. Wir streben nach einer möglichst effizienten Regelüberprüfung für ausdrucksstarke und somit vielfältig einsetzbare Eingabesprachen.

Das Problem der automatisierten Regelüberprüfung kann von zwei Seiten angegangen werden. Einerseits verbessert die theoretische Forschung die Ausdrucksstärke der Eingabesprache für Regeln und entwickelt Algorithmen für diese Sprachen. Die Skalierbarkeit dieser Algorithmen auf grosse Datenmengen wird jedoch oft vernachlässigt. Andererseits implementiert die praktische Forschung skalierbare Algorithmen zur parallelisierten Ausführung in Rechenclustern. Dabei kommt der Entwurf der Eingabesprache oft zu kurz. Unser Projekt vereint beide Ansätze zum beidseitigen Nutzen

Direct link to Lay Summary Last update: 26.07.2017

Lay Summary (French)

Lead
Les procédures opérationnelles de nombreuses autorités et entreprises sont fortement réglementées. Dans la pratique, il est souvent difficile de déterminer le respect effectif de ces règles. Nous développons des algorithmes le contrôlant automatiquement et pouvant faire face à de grandes quantités de données.Nous développons et implémentons des algorithmes parallélisés qui à même de contrôler des données dans un contexte dynamique pour vérifier le respect des règles. Comme entrée, ils reçoivent un flux de données arrivant en temps réel ainsi que les règles à contrôler. Ces dernières sont formulées dans une langue d’entrée définie. Elle doit permettre à ses utilisateurs d’exprimer simplement et de façon intuitive des liens temporels et de contenu entre différents points de données. En cas de violation des règles, il se produit une sortie compacte des données responsables de l’infraction.
Lay summary

La conformité aux règles, ou "compliance", est une tâche importante à laquelle les entreprises consacrent des départements entiers. Ceux-ci doivent parfois, sur la base d’un nombre considérable de journaux d’événements ou de fichiers journaux, contrôler rapidement et de façon fiable que des procédures complexes respectent bien les règles fixées. Une règle typique pour une banque pourrait stipuler qu’un client ne peut pas retirer plus de 5000 francs par semaine. L’identification de certaines infractions a une grande valeur.

Nous développons des algorithmes qui contrôlent en continu des données entrantes pour vérifier si elles contreviennent aux règles. Plus elles sont complexes, plus le contrôle de quantités énormes de données devient difficile. Une langue d’entrée plus ou moins expressive pour les règles gère la complexité réglementaire. Nous visons un contrôle des règles aussi efficace que possible pour des langues d’entrée expressives et pouvant donc s’utiliser de diverses manières.

La poursuite du développement du contrôle automatisé des règles est soumise à un double défi. La recherche théorique améliore d’un côté l’expressivité de la langue d’entrée et développe des algorithmes pour ces langues. L’adaptabilité de ces algorithmes à des grandes quantités de données est toutefois souvent négligée. La recherche appliquée implémente des algorithmes adaptables pour une application parallélisée dans des clusters informatiques, délaissant souvent la conception de la langue d’entrée. Notre projet allie les deux approches, qui en bénéficieront ainsi mutuellement.


Direct link to Lay Summary Last update: 26.07.2017

Lay Summary (English)

Lead
The operational procedures of numerous authorities and companies are subject to strict regulations. In practice, it is often difficult to establish whether the rules in place are actually being complied with. We are developing algorithms that can automatically monitor regulatory compliance and handle large volumes of data.We are developing and implementing efficient, parallelised algorithms capable of monitoring whether data in a dynamic environment comply with given rules. The input for these algorithms is a real-time data feed as well as the rules to be monitored. The rules are formulated in an input language that allows users to express temporal and data dependencies between different events in the data feed in a simple and intuitive manner. If any of the rules are violated, a compact output of the data that caused the violation will be produced
Lay summary

Compliance is a crucial task, and companies have entire departments whose task is to oversee it. Given voluminous log files and other inputs, these departments must quickly and reliably monitor whether the procedures are being followed in compliance with the (possibly complex) rules in force. A typical rule for a bank might be: No customer may withdraw more than 5000 Swiss francs per week. Being able to identify individual violations is of considerable value.

We are developing algorithms that continually monitor incoming data for rule violations. The more complex the rule, the greater the challenge of checking it efficiently against enormous volumes of data. The expressiveness of the input language influences the possible complexity of rules and therefore the efficiency of the monitoring algorithm. Our goal is to find efficient monitoring algorithms for highly expressive and hence practically useful input languages.

The problem of automated rule monitoring can be approached from two directions. On the one hand, theoretical research is improving the expressiveness of the input language for rules and developing algorithms for these languages. However, the scalability of these algorithms to accommodate huge data volumes is frequently neglected. On the other hand, practical research is being conducted on implementing scalable algorithms for parallelised execution in computer clusters. In this context, work on designing input languages often does not receive the attention it merits. Our project combines the two approaches to the benefit of both.


Direct link to Lay Summary Last update: 26.07.2017

Responsible applicant and co-applicants

Employees

Publications

Publication
A Taxonomy for Classifying Runtime Verification Tools
Falcone Yliès, Krstić Srđan, Reger Giles, Traytel Dmitriy (2018), A Taxonomy for Classifying Runtime Verification Tools, in Runtime Verification, 241-262, Springer International Publishing, Cham241-262.
Optimal Proofs for Linear Temporal Logic on Lasso Words
Basin David, Bhatt Bhargav Nagaraja, TraytelDmitriy (2018), Optimal Proofs for Linear Temporal Logic on Lasso Words, in Automated Technology for Verification and Analysis, 37-55, Springer International Publishing, Cham37-55.
Scalable Online First-Order Monitoring
Schneider Joshua, Basin David, Brix Frederik, Krstić Srđan, Traytel Dmitriy (2018), Scalable Online First-Order Monitoring, in Runtime Verification, 353-371, Springer International Publishing, Cham353-371.
Aerial: Almost Event-Rate Independent Algorithms for Monitoring Metric Regular Properties
Basin David, Krstić Srđan, Traytel Dmitriy (2017), Aerial: Almost Event-Rate Independent Algorithms for Monitoring Metric Regular Properties, in RV-CuBES 2017, 3, EasyChair, n.a. 3.
Almost Event-Rate Indepedent Monitoring of Metric Dynamic Logic
Basin David, Krstić Srđan, Traytel Dmitriy (2017), Almost Event-Rate Indepedent Monitoring of Metric Dynamic Logic, in {RV} 2017, 85-102, Springer, Cham85-102.
Almost Event-Rate Indepedent Monitoring of Metric Temporal Logic
Basin David, Bhatt Bhargav Nagaraja, Traytel Dmitriy (2017), Almost Event-Rate Indepedent Monitoring of Metric Temporal Logic, in {TACAS} 2017, 10206, 94-112, Springer, Berlin, Heidelberg 10206, 94-112.
Runtime Verification of Temporal Properties over Out-of-order Data Streams
Basin David, Klaedtke Felix, Zălinescu Eugen (2017), Runtime Verification of Temporal Properties over Out-of-order Data Streams, in Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and , 10426 LNCS, 356-376, Springer, Cham 10426 LNCS, 356-376.

Collaboration

Group / person Country
Types of collaboration
NEC Laboratories Europe, Dr. Felix Klaedtke (see support letter) Germany (Europe)
- in-depth/constructive exchanges on approaches, methods or results
- Industry/business/other use-inspired collaboration

Scientific events

Active participation

Title Type of contribution Title of article or contribution Date Place Persons involved
ATVA 2018 Talk given at a conference Optimal Proofs for Linear Temporal Logic on Lasso Words 07.10.2018 Los Angeles, United States of America Traytel Dmytro;
RV-CuBES 2017 Poster Aerial: Almost Event-Rate Independent Algorithms for Monitoring Metric Regular Properties 15.09.2017 Seattle, United States of America Traytel Dmytro;
RV 2017 Talk given at a conference Almost Event-Rate Independent Monitoring of Metric Dynamic Logic 13.09.2017 Seattle, United States of America Traytel Dmytro;
TACAS 2017 Talk given at a conference Almost Event-Rate Independent Monitoring of Metric Temporal Logic 24.04.2017 Uppsala, Sweden Bhatt Bhargav Nagaraja;


Abstract

We will develop methods for determining whether a large quantity of steadily arriving data is well-behaved with respect to a given specification-the (Online) Monitoring Problem. The Monitoring Problem can be phrased as follows: Given a stream of time-varying data, called events, and a property formulated in a specification language, check whether the property is satisfied for every prefix of the stream. If the property is not always satisfied, the monitor should report the violating events. We will develop and implement efficient and scalable algorithms solving the Monitoring Problem for expressive logic-based specification languages and high-velocity and voluminous streams of data.
-