Bounded-Memory Runtime Enforcement
| Autor: | Shankar, Saumya, Rollet, Antoine, Pinisetty, Srinivas, Falcone, Yliès |
|---|---|
| Přispěvatelé: | Indian Institute of technology Bhubaneswar, Laboratoire Bordelais de Recherche en Informatique (LaBRI), Université de Bordeaux (UB)-École Nationale Supérieure d'Électronique, Informatique et Radiocommunications de Bordeaux (ENSEIRB)-Centre National de la Recherche Scientifique (CNRS), Compiler Optimization and Run-time Systems (CORSE), Inria Grenoble - Rhône-Alpes, Institut National de Recherche en Informatique et en Automatique (Inria)-Institut National de Recherche en Informatique et en Automatique (Inria)-Laboratoire d'Informatique de Grenoble (LIG), Centre National de la Recherche Scientifique (CNRS)-Université Grenoble Alpes (UGA)-Institut polytechnique de Grenoble - Grenoble Institute of Technology (Grenoble INP ), Université Grenoble Alpes (UGA)-Centre National de la Recherche Scientifique (CNRS)-Université Grenoble Alpes (UGA)-Institut polytechnique de Grenoble - Grenoble Institute of Technology (Grenoble INP ), Université Grenoble Alpes (UGA), ANR-20-CE39-0009,SEVERITAS,Systèmes de tests et evaluations sûrs et vérifiables(2020) |
| Rok vydání: | 2022 |
| Předmět: | |
| Zdroj: | Model Checking Software ISBN: 9783031150760 SPIN 2022-28th International Symposium on Model Checking of Software SPIN 2022-28th International Symposium on Model Checking of Software, May 2022, Chicago, United States. pp.114-133, ⟨10.1007/978-3-031-15077-7_7⟩ |
| DOI: | 10.1007/978-3-031-15077-7_7 |
| Popis: | International audience; Runtime Enforcement (RE) is a monitoring technique to ensure that a system obeys a set of formal requirements (properties). RE employs an enforcer (a safety wrapper for the system) which modifies the (untrustworthy) output by performing actions such as delaying (by storing/buffering) and suppressing events, when needed. In this paper, to handle practical applications with memory constraints, we propose a new RE paradigm where the memory of the enforcer is bounded/finite. Besides the property to be enforced, the user specifies a bound on the enforcer memory. Bounding the memory poses various challenges such as how to handle the situation when the memory is full, how to optimally discard events from the buffer to accommodate new events and let the enforcer continue operating. We define the bounded-memory RE problem and develop a framework for any regular property. The proposed framework is implemented and its performance evaluated via some examples from application scenarios indicates that the enforcer has reasonable execution time overhead. |
| Databáze: | OpenAIRE |
| Externí odkaz: |
|