Scalable offline monitoring of temporal specifications

Publikationstyp
Journal Article
Date Issued
2016-03-07
Sprache
English
Author(s)
Basin, David  
Caronni, Germano  
Ereth, Sarah  
Harvan, Matúš  
Klaedtke, Felix Christopher  
Mantel, Heiko 
TORE-URI
http://hdl.handle.net/11420/13823
Journal
Formal methods in system design  
Volume
49
Issue
1-2
Start Page
75
End Page
108
Citation
Formal Methods in System Design 49 (1-2): 75-108 (2016-10-01)
Publisher DOI
10.1007/s10703-016-0242-y
Scopus ID
2-s2.0-84960122916
Publisher
Springer Science + Business Media B.V
We propose an approach to monitoring IT systems offline where system actions are logged in a distributed file system and subsequently checked for compliance against policies formulated in an expressive temporal logic. The novelty of our approach is that monitoring is parallelized so that it scales to large logs. Our technical contributions comprise a formal framework for slicing logs, an algorithmic realization based on MapReduce, and a high-performance implementation. We evaluate our approach analytically and experimentally, proving the soundness and completeness of our slicing techniques and demonstrating its practical feasibility and efficiency on real-world logs with 400 GB of relevant data.
Subjects
MapReduce
Monitoring
Temporal Logic
Verification
DDC Class
004: Informatik