rv12

S. Pinisetty, Y. Falcone, T. Jéron, H. Marchand, A. Rollet, O. Nguena Timo. Runtime Enforcement of Timed Properties. In Third International Conference on Runtime Verification RV 2012, Istanbul, Turkey, September 2012.

Download [help]

Download paper: Adobe portable document (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 is a powerful technique to ensure that a running system respects some desired properties. Using an enforcement monitor, an (untrusted) input execution (in the form of a sequence of events) is modified into an output sequence that complies to a property. Runtime enforcement has been extensively studied over the last decade in the context of untimed properties. This paper introduces runtime enforcement of timed properties. We revisit the foundations of runtime enforcement when time between events matters.We show how runtime enforcers can be synthesized for any safety or co-safety timed property. Proposed runtime enforcers are time retardant: to produce an output sequence, additional delays are introduced between the events of the input sequence to correct it. Runtime enforcers have been prototyped and our simulation experiments validate their effectiveness

Contact

Thierry Jéron http://www.irisa.fr/prive/jeron
Hervé Marchand http://www.irisa.fr/prive/hmarchan

BibTex Reference

@InProceedings{rv12,
   Author = {Pinisetty, S. and Falcone, Y. and Jéron, T. and Marchand, H. and Rollet, A. and Nguena Timo, O.},
   Title = {Runtime Enforcement of Timed Properties},
   BookTitle = {Third International Conference on Runtime Verification RV 2012},
   Address = {Istanbul, Turkey},
   Month = {September},
   Year = {2012}
}

EndNote Reference [help]

Get EndNote Reference (.ref)