Jump to : Download | Abstract | Contact | BibTex reference | EndNote reference |

wodes-TE

S. Pinisetty, Y. Falcone, T. Jéron, H. Marchand. Runtime Enforcement of Parametric Timed Properties with Practical Applications. In IEEE International Workshop on Discrete Event Systems, Pages 420-427, Cachan, France, May 2014.

Download [help]

Download paper: Adobe portable document (pdf) pdf

Copyright notice: This material is presented to ensure timely dissemination of scholarly and technical work. Copyright and all rights therein are retained by authors or by other copyright holders. All persons copying this information are expected to adhere to the terms and constraints invoked by each author's copyright. These works may not be reposted without the explicit permission of the copyright holder.
This page is automatically generated by bib2html v216, © INRIA 2002-2007, Projet Lagadic

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

Contact

Thierry Jéron http://www.irisa.fr/prive/jeron
Hervé Marchand http://people.rennes.inria.fr/Herve.Marchand/

BibTex Reference

@InProceedings{wodes-TE,
   Author = {Pinisetty, S. and Falcone, Y. and Jéron, T. and Marchand, H.},
   Title = {Runtime Enforcement of Parametric Timed Properties with Practical Applications},
   BookTitle = {IEEE International Workshop on Discrete Event Systems},
   Pages = {420--427},
   Address = {Cachan, France},
   Month = {May},
   Year = {2014}
}

EndNote Reference [help]

Get EndNote Reference (.ref)