Abstract | ||
---|---|---|
We leverage Büchi games for the runtime enforcement of regular properties with uncontrollable events. Runtime enforcement consists in modifying the execution of a running system to have it satisfy a given regular property, modelled by an automaton. We revisit runtime enforcement with uncontrollable events and propose a framework where we model the runtime enforcement problem as a Büchi game and synthesise sound, compliant, and optimal enforcement mechanisms as strategies.We present algorithms and a tool implementing enforcement mechanisms.We reduce the complexity of the computations performed by enforcement mechanisms at runtime by pre-computing the decisions of enforcement mechanisms ahead of time. |
Year | DOI | Venue |
---|---|---|
2017 | 10.1145/3092282.3092296 | SPIN |
Keywords | DocType | ISBN |
Runtime Verification,Runtime Enforcement,Games,Automata | Conference | 978-1-4503-5077-8 |
Citations | PageRank | References |
1 | 0.35 | 7 |
Authors | ||
3 |
Name | Order | Citations | PageRank |
---|---|---|---|
Matthieu Renard | 1 | 9 | 1.84 |
Antoine Rollet | 2 | 62 | 9.53 |
Yliès Falcone | 3 | 508 | 39.21 |