Correct and Efficient Policy Monitoring, a Retrospective
Research output: Chapter in Book/Report/Conference proceeding › Article in proceedings › Research › peer-review
Standard
Correct and Efficient Policy Monitoring, a Retrospective. / Basin, David; Krstić, Srđan; Schneider, Joshua; Traytel, Dmitriy.
Automated Technology for Verification and Analysis - 21st International Symposium, ATVA 2023, Proceedings. ed. / Étienne André; Jun Sun. Springer, 2023. p. 3-30 (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics), Vol. 14215 LNCS).Research output: Chapter in Book/Report/Conference proceeding › Article in proceedings › Research › peer-review
Harvard
APA
Vancouver
Author
Bibtex
}
RIS
TY - GEN
T1 - Correct and Efficient Policy Monitoring, a Retrospective
AU - Basin, David
AU - Krstić, Srđan
AU - Schneider, Joshua
AU - Traytel, Dmitriy
N1 - Publisher Copyright: © 2023, The Author(s), under exclusive license to Springer Nature Switzerland AG.
PY - 2023
Y1 - 2023
N2 - 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.
AB - 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.
KW - monitoring
KW - runtime verification
KW - temporal logic
UR - http://www.scopus.com/inward/record.url?scp=85175964999&partnerID=8YFLogxK
U2 - 10.1007/978-3-031-45329-8_1
DO - 10.1007/978-3-031-45329-8_1
M3 - Article in proceedings
AN - SCOPUS:85175964999
SN - 9783031453281
T3 - Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
SP - 3
EP - 30
BT - Automated Technology for Verification and Analysis - 21st International Symposium, ATVA 2023, Proceedings
A2 - André, Étienne
A2 - Sun, Jun
PB - Springer
T2 - 21st International Symposium on Automated Technology for Verification and Analysis, ATVA 2023
Y2 - 24 October 2023 through 27 October 2023
ER -
ID: 373513326