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
关键词
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 条
  • [41] Linear-Time Algorithms for Proportional Apportionment
    Cheng, Zhanpeng
    Eppstein, David
    ALGORITHMS AND COMPUTATION, ISAAC 2014, 2014, 8889 : 581 - 592
  • [42] A LINEAR-TIME ALGORITHM FOR FINDING AN AMBITUS
    MISHRA, B
    TARJAN, RE
    ALGORITHMICA, 1992, 7 (5-6) : 521 - 554
  • [43] A linear-time algorithm for the generation of trees
    Alonso, L
    Remy, JL
    Schott, R
    ALGORITHMICA, 1997, 17 (02) : 162 - 182
  • [44] Linear-time Minimization of Wheeler DFAs
    Alanko, Jarno
    Cotumaccio, Nicola
    Prezza, Nicola
    DCC 2022: 2022 DATA COMPRESSION CONFERENCE (DCC), 2022, : 53 - 62
  • [45] A Coalgebraic Approach to Linear-Time Logics
    Cirstea, Corina
    FOUNDATIONS OF SOFTWARE SCIENCE AND COMPUTATION STRUCTURES, 2014, 8412 : 426 - 440
  • [46] A Paraconsistent Linear-time Temporal Logic
    Kamide, Norihiro
    Wansing, Heinrich
    FUNDAMENTA INFORMATICAE, 2011, 106 (01) : 1 - 23
  • [47] Linear-Time Oblivious Permutations for SPDZ
    Laud, Peeter
    CRYPTOLOGY AND NETWORK SECURITY, CANS 2021, 2021, 13099 : 245 - 252
  • [48] Linear-time algorithms for eliminating claws in graphs
    Bonomo-Braberman, Flavia
    Nascimento, Julliano R.
    Oliveira, Fabiano S.
    Souza, Ueverton S.
    Szwarcfiter, Jayme L.
    INTERNATIONAL TRANSACTIONS IN OPERATIONAL RESEARCH, 2024, 31 (01) : 296 - 315
  • [49] Linear-time error calculation for approximate adders
    Rezaalipour, Morteza
    Dehyadegari, Masoud
    COMPUTERS & ELECTRICAL ENGINEERING, 2021, 92 (92)
  • [50] Linear-Time Algorithms for Tree Root Problems
    Chang, Maw-Shang
    Ko, Ming-Tat
    Lu, Hsueh-I
    ALGORITHMICA, 2015, 71 (02) : 471 - 495