Correct and Efficient Policy Monitoring, a Retrospective

Research output: Chapter in Book/Report/Conference proceedingArticle in proceedingsResearchpeer-review

The MonPoly project started over a decade ago to build effective tools for monitoring trace properties, including functional correctness, security, and compliance policies. The original MonPoly tool supported monitoring specifications given in metric first-order temporal logic, an expressive specification language. It handled both the online case, where system events are monitored as they occur, and the offline case, monitoring logs. Our tool has evolved over time into a family of tools and supporting infrastructure to make monitoring both scalable and suitable for high assurance applications. We survey this evolution which includes: (1) developing more expressive monitors, e.g., adding aggregation operators, regular expressions, and limited forms of recursion; (2) delimiting efficiently monitorable fragments and designing new monitoring algorithms for them; (3) supporting parallel and distributed monitoring; (4) using theorem proving to verify monitoring algorithms and explore extensions; and (5) carrying out ambitious case studies.

Original languageEnglish
Title of host publicationAutomated Technology for Verification and Analysis - 21st International Symposium, ATVA 2023, Proceedings
EditorsÉtienne André, Jun Sun
PublisherSpringer
Publication date2023
Pages3-30
ISBN (Print)9783031453281
DOIs
Publication statusPublished - 2023
Event21st International Symposium on Automated Technology for Verification and Analysis, ATVA 2023 - Singapore, Singapore
Duration: 24 Oct 202327 Oct 2023

Conference

Conference21st International Symposium on Automated Technology for Verification and Analysis, ATVA 2023
LandSingapore
BySingapore
Periode24/10/202327/10/2023
SeriesLecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
Volume14215 LNCS
ISSN0302-9743

Bibliographical note

Publisher Copyright:
© 2023, The Author(s), under exclusive license to Springer Nature Switzerland AG.

    Research areas

  • monitoring, runtime verification, temporal logic

ID: 373513326