Runtime Enforcement of Parametric Timed Properties with Practical Applications

Abstract : Runtime enforcement (RE) is a technique where a so-called monitor modifies the execution of a system to comply with a desired property. RE consists in using a so called monitor to modify an input sequence of events so that it complies with the property. Very few convincing applications of runtime enforcement have been proposed so far since most of the proposed approaches remain on the theoretical level. In network security, RE monitors can detect and prevent Denial-of-Service attacks. In resource allocation, RE monitors can ensure fairness. Specifications in these domains express data-constraints over the received events where the timing between events matters. To formalize these requirements, we introduce Parameterized Timed Automata with Variables (PTAVs), an extension of Timed Automata (TAs) with internal and external variables. We then extend enforcement for TAs to enforcement for PTAVs. We model requirements from the considered application domains and show how enforcement monitors can ensure system correctness w.r.t. these requirements. Finally, we propose a prototype implementation to experiment RE monitors on some properties. Our experiments and the performance of RE monitors demonstrate the feasibility of our approach.
Document type :
Conference papers
Complete list of metadatas

Cited literature [16 references]  Display  Hide  Download

https://hal.inria.fr/hal-00974548
Contributor : Hervé Marchand <>
Submitted on : Monday, April 7, 2014 - 10:37:34 AM
Last modification on : Thursday, February 7, 2019 - 2:21:50 PM
Long-term archiving on : Monday, July 7, 2014 - 11:03:29 AM

File

2014-wodes-TE.pdf
Files produced by the author(s)

Identifiers

  • HAL Id : hal-00974548, version 1

Citation

Srinivas Pinisetty, Yliès Falcone, Thierry Jéron, Hervé Marchand. Runtime Enforcement of Parametric Timed Properties with Practical Applications. IEEE International Workshop on Discrete Event Systems, May 2014, Cachan, France. pp.420-427. ⟨hal-00974548⟩

Share

Metrics

Record views

745

Files downloads

270