TY - JOUR
T1 - A monitoring tool for linear-time μHML
AU - Aceto, Luca
AU - Achilleos, Antonis
AU - Attard, Duncan Paul
AU - Exibard, Léo
AU - Francalanza, Adrian
AU - Ingólfsdóttir, Anna
N1 - Publisher Copyright:
© 2023 Elsevier B.V.
PY - 2024/1
Y1 - 2024/1
N2 - We present detectEr, a monitoring tool that targets software applications written for Erlang/OTP. The tool runtime checks specifications expressed in a safety fragment of the linear-time modal μ-calculus called [Formula presented], used to describe properties about the current system execution. Our technical development is founded on previous theoretical results that are lifted to a first-order setting, where systems produce executions containing events that carry data. We overview the main features of detectEr, showing how properties can be flexibly written and synthesised as executable Erlang monitors that can be instrumented with the running system.
AB - We present detectEr, a monitoring tool that targets software applications written for Erlang/OTP. The tool runtime checks specifications expressed in a safety fragment of the linear-time modal μ-calculus called [Formula presented], used to describe properties about the current system execution. Our technical development is founded on previous theoretical results that are lifted to a first-order setting, where systems produce executions containing events that carry data. We overview the main features of detectEr, showing how properties can be flexibly written and synthesised as executable Erlang monitors that can be instrumented with the running system.
KW - Linear-time properties
KW - Monitor synthesis
KW - Runtime verification
UR - http://www.scopus.com/inward/record.url?scp=85173579453&partnerID=8YFLogxK
U2 - 10.1016/j.scico.2023.103031
DO - 10.1016/j.scico.2023.103031
M3 - Article
AN - SCOPUS:85173579453
SN - 0167-6423
VL - 232
JO - Science of Computer Programming
JF - Science of Computer Programming
M1 - 103031
ER -