GREP: Games for the Runtime Enforcement of Properties

The paper entitled GREP: Games for the Runtime Enforcement of Properties has been accepted for publication in the proceedings of ICTSS 2017, the 29th IFIP International Conference on Testing Software and Systems.

Below is an abstract of the paper:

We present GREP, a tool for the runtime enforcement of (timed) properties. GREP takes an execution sequence as input (stdin), and modifies it (stdout) as necessary to enforce the desired property, when possible. GREP can enforce any regular timed property described by a deterministic and complete Timed Automaton. The main novelties of GREP are twofold: it uses game theory to improve the synthesis of enforcement mechanisms, and it accounts for uncontrollable events, i.e. events that cannot be controlled by the enforcement mechanisms and thus have to be released immediately. We present an overview of GREP and validate its usability with a performance evaluation.

This is joint work with Matthieu Renard and Antoine Rollet from University of Bordeaux.

The pre-print of the paper can be downloaded here.