Monitoring of temporal first-order properties with aggregations
Basin, David ; Klaedtke, Felix ; Marinovic, Srdjan ; Zălinescu, Eugen
In: Formal Methods in System Design, 2015, vol. 46, no. 3, p. 262-285
Ajouter à la liste personnelle- Summary
- 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.