Treffer: A monitoring tool for linear-time 𝜇HML
Title:
A monitoring tool for linear-time 𝜇HML
Authors:
Publisher Information:
Elsevier
Publication Year:
2024
Collection:
University of Malta: OAR@UM / L-Università ta' Malta
Subject Terms:
Document Type:
Fachzeitschrift
article in journal/newspaper
Language:
English
DOI:
10.1016/j.scico.2023.103031
Availability:
Rights:
info:eu-repo/semantics/restrictedAccess ; The copyright of this work belongs to the author(s)/publisher. The rights of this work are as defined by the appropriate Copyright Legislation or as modified by any successive legislation. Users may access this work and can make use of the information contained in accordance with the Copyright Legislation provided that the author must be properly acknowledged. Further distribution or reproduction in any format is prohibited without the prior permission of the copyright holder.
Accession Number:
edsbas.D6507619
Database:
BASE
Weitere Informationen
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 MAXHMLD, 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. ; peer-reviewed