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

renard:hal-01185238

M. Renard, Y. Falcone, A. Rollet, S. Pinisetty, T. Jéron, H. Marchand. Enforcement of (Timed) Properties with Uncontrollable Events. In 12th International Colloquium on Theoretical Aspects of Computing (ICTAC 2015), Theoretical Aspects of Computing - ICTAC 2015, Volume LNCS, Cali, Colombia, October 2015.

Download [help]

Download paper: Doi page

Download paper: (link)

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

This paper deals with runtime enforcement of untimed and timed properties with uncontrollable events. Runtime enforcement consists in modifying the executions of a running system to ensure their correctness with respect to a desired property. We introduce a framework that takes as input any regular (timed) property over an alphabet of events, with some of these events being uncontrollable. An uncontrollable event cannot be delayed nor intercepted by an enforcement mechanism. Enforcement mechanisms satisfy important properties, namely soundness and compliance, meaning that enforcement mechanisms output correct executions that are close to the input execution. We discuss the conditions for a property to be enforceable with uncontrollable events, and we define enforcement mechanisms that modify executions to obtain a correct output, as soon as possible. Moreover, we synthesize sound and compliant descriptions of runtime enforcement mechanisms at two levels of abstraction to facilitate their design and implementation

Contact

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

BibTex Reference

@InProceedings{renard:hal-01185238,
   Author = {Renard, M. and Falcone, Y. and Rollet, A. and Pinisetty, S. and Jéron, T. and Marchand, H.},
   Title = {Enforcement of (Timed) Properties with Uncontrollable Events},
   BookTitle = {12th International Colloquium on Theoretical Aspects of Computing (ICTAC 2015)},
   Volume = {LNCS},
   Number = {9399},
   Series = {Theoretical Aspects of Computing - ICTAC 2015},
   Publisher = {Springer},
   Address = {Cali, Colombia},
   Month = {October},
   Year = {2015}
}

EndNote Reference [help]

Get EndNote Reference (.ref)