Fulltext

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
    Titre
    • Monitoring of temporal first-order properties with aggregations
    Auteur
    • Basin, David. Computer Science Department, Institute of Information Security, ETH Zurich, Universiätstr 6, 8092, Zurich, Switzerland
    • Klaedtke, Felix. NEC Europe Ltd., Kurfürsten-Anlage 36, 69115, Heidelberg, Germany
    • Marinovic, Srdjan. Computer Science Department, Institute of Information Security, ETH Zurich, Universiätstr 6, 8092, Zurich, Switzerland
    • Zălinescu, Eugen. Computer Science Department, Institute of Information Security, ETH Zurich, Universiätstr 6, 8092, Zurich, Switzerland
    Type de document
    • Postprint
    Langue
    • Anglais
    Publié dans
    • Formal Methods in System Design, 2015, vol. 46, no. 3, p. 262-285. Springer US; http://www.springer-ny.com
    Autre version électronique
    Identifiant OAI-PMH
    • oai:doc.rero.ch:331126
    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.