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 条
  • [1] A Monitoring Tool for Linear-Time μHML
    Aceto, Luca
    Achilleos, Antonis
    Attard, Duncan Paul
    Exibard, Leo
    Francalanza, Adrian
    Ingolfsdottir, Anna
    COORDINATION MODELS AND LANGUAGES, 2022, 13271 : 200 - 219
  • [2] Linear-time tool for evaluating consistent hashing: EVT
    Kong, Xiangsheng
    Gao, Weixue
    Journal of Chemical and Pharmaceutical Research, 2014, 6 (06) : 2945 - 2949
  • [3] A Linear-time Graph Kernel
    Hido, Shohei
    Kashima, Hisashi
    2009 9TH IEEE INTERNATIONAL CONFERENCE ON DATA MINING, 2009, : 179 - 188
  • [4] Linear-time transitive orientation
    McConnell, RM
    Spinrad, JP
    PROCEEDINGS OF THE EIGHTH ANNUAL ACM-SIAM SYMPOSIUM ON DISCRETE ALGORITHMS, 1997, : 19 - 25
  • [5] Linear-Time Limited Automata
    Guillon, Bruno
    Prigioniero, Luca
    DESCRIPTIONAL COMPLEXITY OF FORMAL SYSTEMS, DCFS 2018, 2018, 10952 : 126 - 138
  • [6] PROJECTIVE PLANARITY IN LINEAR-TIME
    MOHAR, B
    JOURNAL OF ALGORITHMS-COGNITION INFORMATICS AND LOGIC, 1993, 15 (03): : 482 - 502
  • [7] The Density of Linear-Time Properties
    Finkbeiner, Bernd
    Torfah, Hazem
    AUTOMATED TECHNOLOGY FOR VERIFICATION AND ANALYSIS (ATVA 2017), 2017, 10482 : 139 - 155
  • [8] Linear-Time Verification of Firewalls
    Acharya, H. B.
    Gouda, M. G.
    2009 17TH IEEE INTERNATIONAL CONFERENCE ON NETWORK PROTOCOLS (ICNP 2009), 2009, : 133 - 140
  • [9] Events in linear-time properties
    Paun, DO
    Chechik, M
    IEEE INTERNATIONAL SYMPOSIUM ON REQUIREMENTS ENGINEERING, PROCEEDINGS, 1999, : 123 - 132
  • [10] Linear-time limited automata
    Guillon, Bruno
    Prigioniero, Luca
    THEORETICAL COMPUTER SCIENCE, 2019, 798 : 95 - 108
12345