A monitoring tool for linear-time μHML

被引：1
|
作者：
Aceto, Luca [2 ,3 ]
Achilleos, Antonis [2 ]
Attard, Duncan Paul [1 ,2 ]
Exibard, Leo [2 ]
Francalanza, Adrian [1 ]
Ingolfsdottir, Anna [2 ]
机构：
[1] Univ Malta, Msida, Malta
[2] Reykjavik Univ, Reykjavik, Iceland
[3] Gran Sasso Sci Inst, Laquila, Italy
来源：
SCIENCE OF COMPUTER PROGRAMMING | 2024年 / 232卷
关键词：
Runtime verification; Linear-time properties; Monitor synthesis;
D O I：
10.1016/j.scico.2023.103031
中图分类号：
TP31 [计算机软件];
学科分类号：
081202 ; 0835 ;
摘要：
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 mu-calculus called MAXHML(D), 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.
引用
收藏
页数：7
相关论文
共 50 条
  • [21] Synchronized Linear-Time Temporal Logic
    Heinrich Wansing
    Norihiro Kamide
    Studia Logica, 2011, 99
  • [22] Linear-Time Minimal Cograph Editing
    Crespelle, Christophe
    FUNDAMENTALS OF COMPUTATION THEORY, FCT 2021, 2021, 12867 : 176 - 189
  • [23] Phase semantics for linear-time formalism
    Kamide, Norihiro
    LOGIC JOURNAL OF THE IGPL, 2011, 19 (01) : 121 - 143
  • [24] LINEAR-TIME DIVIDER ARRAY.
    Williams, J.
    Hamacher, V.C.
    Canadian electrical engineering journal, 1981, 6 (04): : 14 - 20
  • [25] RECOGNIZING AN ENVELOPE OF LINES IN LINEAR-TIME
    GUEVREMONT, E
    SNOEYINK, J
    LECTURE NOTES IN COMPUTER SCIENCE, 1992, 650 : 370 - 377
  • [26] Linear-time algorithm for the generation of trees
    Algorithmica (New York), 1997, 17 (02):
  • [27] A Linear-Time Algorithm for Seeds Computation
    Kociumaka, Tomasz
    Kubica, Marcin
    Radoszewski, Jakub
    Rytter, Wojciech
    Walen, Tomasz
    ACM TRANSACTIONS ON ALGORITHMS, 2020, 16 (02)
  • [28] Constructive completeness for the linear-time μ-calculus
    Doumane, Amina
    2017 32ND ANNUAL ACM/IEEE SYMPOSIUM ON LOGIC IN COMPUTER SCIENCE (LICS), 2017,
  • [29] A LINEAR-TIME SCHEME FOR VERSION RECONSTRUCTION
    YU, L
    ROSENKRANTZ, DJ
    ACM TRANSACTIONS ON PROGRAMMING LANGUAGES AND SYSTEMS, 1994, 16 (03): : 775 - 797
  • [30] Simple Linear-Time Repetition Factorization
    Yonemoto, Yuki
    Inenaga, Shunsuke
    STRING PROCESSING AND INFORMATION RETRIEVAL, SPIRE 2024, 2025, 14899 : 348 - 361
12345