Name
Abstract | ||
|---|---|---|
AbstractAbstractThis paper deals with runtime enforcement of timed properties withuncontrollable events. Runtime enforcement consists in defining andusing an enforcement mechanism that modifies the executions of a runningsystem to ensure their correctness with respect to the desiredproperty. Uncontrollable events cannot be modified by theenforcement mechanisms and thus have to be released immediately. Wepresent a complete theoretical framework for synthesising suchmechanism, modelling the runtime enforcement problem as a Büchigame. It permits to pre-compute the decisions of the enforcementmechanism, thus avoiding to explore the whole execution tree atruntime.The obtained enforcement mechanism issound, compliant and optimal, meaning that it should output as soon aspossible correct executions that are as close as possible to the inputexecution. This framework takes as input any timed regular propertymodelled by a timed automaton.We present GREP, a tool implementing this approach. We providealgorithms and implementation details of the different modules ofGREP, and evaluate its performance. The results are comparedwith another state of the art runtime enforcement tool. |
Year | DOI | Venue |
|---|---|---|
2020 | 10.1007/s00165-020-00515-2 | Formal Aspects of Computing |
Keywords | DocType | Volume |
Runtime Enforcement,Runtime Verification,Games,Timed Automata | Journal | 32 |
Issue | ISSN | Citations |
2-3 | 0934-5043 | 0 |
PageRank | References | Authors |
0.34 | 0 | 3 |
Name | Order | Citations | PageRank |
|---|---|---|---|
| Matthieu Renard | 1 | 9 | 1.84 |
| Antoine Rollet | 2 | 62 | 9.53 |
| Yliès Falcone | 3 | 508 | 39.21 |