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 条
  • [31] THE LINEAR-TIME RECOGNITION OF DIGITAL ARCS
    DAMASCHKE, P
    PATTERN RECOGNITION LETTERS, 1995, 16 (05) : 543 - 548
  • [32] Linear-time computation of local periods
    Duval, JP
    Kolpakov, R
    Kucherov, G
    Lecroq, T
    Lefebvre, A
    THEORETICAL COMPUTER SCIENCE, 2004, 326 (1-3) : 229 - 240
  • [33] Linear-Time Reductions of Resolution Proofs
    Bar-Ilan, Omer
    Fuhrmann, Oded
    Hoory, Shlomo
    Shacham, Ohad
    Strichman, Ofer
    HARDWARE AND SOFTWARE: VERIFICATION AND TESTING, PROCEEDINGS, 2009, 5394 : 114 - +
  • [34] LINEAR-TIME LOGICS - A COALGEBRAIC PERSPECTIVE
    Cirstea, Corina
    LOGICAL METHODS IN COMPUTER SCIENCE, 2024, 20 (02) : 1 - 13
  • [35] EVOLVING ALGEBRAS AND LINEAR-TIME HIERARCHY
    BLASS, A
    GUREVICH, Y
    INFORMATION PROCESSING '94, VOL I: TECHNOLOGY AND FOUNDATIONS, 1994, 51 : 383 - 390
  • [36] An efficient linear-time clustering algorithms
    Wang, L
    Zang, LJ
    Song, RF
    Proceedings of the 11th Joint International Computer Conference, 2005, : 678 - 681
  • [37] A linear-time majority tree algorithm
    Amenta, N
    Clarke, F
    John, KS
    ALGORITHMS IN BIOINFORMATICS, PROCEEDINGS, 2003, 2812 : 216 - 227
  • [38] A linear-time algorithm for the generation of trees
    L. Alonso
    J. L. Rémy
    R. Schott
    Algorithmica, 1997, 17 : 162 - 182
  • [39] Dense Linear-Time Correspondences for Tracking
    Obdrzalek, Stepan
    Perdoch, Michal
    Matas, Jiri
    2008 IEEE COMPUTER SOCIETY CONFERENCE ON COMPUTER VISION AND PATTERN RECOGNITION WORKSHOPS, VOLS 1-3, 2008, : 1302 - 1309
  • [40] CAYLEY LINEAR-TIME COMPUTABLE GROUPS
    Kruengthomya, Prohrak
    Berdinsky, Dmitry
    GROUPS COMPLEXITY CRYPTOLOGY, 2023, 15 (02)