DECENT: A Benchmark for Decentralized Enforcement

被引:1
|
作者
Gallay, Florian [1 ]
Falcone, Ylies [1 ]
机构
[1] Univ Grenoble Alpes, CNRS, Grenoble INP, Inria,LIG, F-38000 Grenoble, France
来源
RUNTIME VERIFICATION (RV 2022) | 2022年 / 13498卷
关键词
RUNTIME ENFORCEMENT; TIMED PROPERTIES;
D O I
10.1007/978-3-031-17196-3_18
中图分类号
TP3 [计算技术、计算机技术];
学科分类号
0812 ;
摘要
DECENT is a benchmark for evaluating decentralized enforcement. It implements two enforcement algorithms that differ in their strategy for correcting the execution: the first one explores all alternatives to perform a globally optimal correction, while the second follows an incremental strategy based on locally optimal choices. Decent allows comparing these algorithms with a centralized enforcement algorithm in terms of computational metrics and metrics for decentralized monitoring such as the number and size of messages or the required computation on each component. Our experiments show that (i) the number of messages sent and the internal memory usage is much smaller with decentralized algorithms (ii) the locally optimal algorithm performs closely to the globally optimal one.
引用
收藏
页码:293 / 303
页数:11
相关论文
共 50 条
  • [1] Decentralized LTL Enforcement
    Gallay, Florian
    Falcone, Ylies
    ELECTRONIC PROCEEDINGS IN THEORETICAL COMPUTER SCIENCE, 2021, (346): : 135 - 151
  • [2] Decentralized runtime enforcement for robotic swarms
    Hu, Chi
    Dong, Wei
    Yang, Yong-hui
    Shi, Hao
    Deng, Fei
    FRONTIERS OF INFORMATION TECHNOLOGY & ELECTRONIC ENGINEERING, 2020, 21 (11) : 1591 - 1606
  • [3] Decentralized runtime enforcement for robotic swarms
    Chi Hu
    Wei Dong
    Yong-hui Yang
    Hao Shi
    Fei Deng
    Frontiers of Information Technology & Electronic Engineering, 2020, 21 : 1591 - 1606
  • [4] Decentralized deadlock-free enforcement of message orderings in message-based systems
    Samadi, Mahboubeh
    Ghassemi, Fatemeh
    Khosravi, Ramtin
    JOURNAL OF COMPUTER AND SYSTEM SCIENCES, 2024, 144
  • [5] Predictive runtime enforcement
    Pinisetty, Srinivas
    Preoteasa, Viorel
    Tripakis, Stavros
    Jeron, Thierry
    Falcone, Ylies
    Marchand, Herve
    FORMAL METHODS IN SYSTEM DESIGN, 2017, 51 (01) : 154 - 199
  • [6] Compositional runtime enforcement revisited
    Pinisetty, Srinivas
    Pradhan, Ankit
    Roop, Partha
    Tripakis, Stavros
    FORMAL METHODS IN SYSTEM DESIGN, 2021, 59 (1-3) : 205 - 252
  • [7] Runtime enforcement of timed properties revisited
    Pinisetty, Srinivas
    Falcone, Ylies
    Jeron, Thierry
    Marchand, Herve
    Rollet, Antoine
    Timo, Omer Nguena
    FORMAL METHODS IN SYSTEM DESIGN, 2014, 45 (03) : 381 - 422
  • [8] Runtime Enforcement using Buchi Games
    Renard, Matthieu
    Rollet, Antoine
    Falcone, Ylies
    SPIN'17: PROCEEDINGS OF THE 24TH ACM SIGSOFT INTERNATIONAL SPIN SYMPOSIUM ON MODEL CHECKING OF SOFTWARE, 2017, : 70 - 79
  • [9] Bounded-Memory Runtime Enforcement
    Shankar, Saumya
    Rollet, Antoine
    Pinisetty, Srinivas
    Falcone, Ylies
    MODEL CHECKING SOFTWARE, SPIN 2022, 2022, 13255 : 114 - 133
  • [10] Runtime enforcement of timed properties revisited
    Srinivas Pinisetty
    Yliès Falcone
    Thierry Jéron
    Hervé Marchand
    Antoine Rollet
    Omer Nguena Timo
    Formal Methods in System Design, 2014, 45 : 381 - 422