Runtime Enforcement Monitors: composition, synthesis, and enforcement abilities

Yliès Falcone (1) , Laurent Mounier (2) , Jean-Claude Fernandez (2) , Jean-Luc Richier (3)

1 VERTECS - Verification models and techniques applied to testing and control of reactive systems
2 VERIMAG - IMAG - VERIMAG
3 VASCO - Validation de Systèmes, Composants et Objets logiciels

Runtime enforcement is a powerful technique to ensure that a program will respect a given set of properties. We extend previous work on this topic in several directions. Firstly, we propose a generic notion of enforcement monitors based on a memory device and finite sets of control states and enforcement operations. Moreover, we specify their enforcement abilities w.r.t. the general Safety-Progress classification of properties. Furthermore, we propose a systematic technique to produce a monitor from the automaton recognizing a given safety, guarantee, obligation or response property. Finally, we show that this notion of enforcement monitors is more amenable to implementation and encompasses previous runtime enforcement mechanisms.

Mots clés: Runtime enforcement; Monito; Safety-progress classification; Monitor synthesis; Composition

Domaines: Systèmes embarqués

Yliès Falcone, Laurent Mounier, Jean-Claude Fernandez, Jean-Luc Richier. Runtime Enforcement Monitors: composition, synthesis, and enforcement abilities. Formal Methods in System Design, 2011, 38 (3), pp.223-262. ⟨10.1007/s10703-011-0114-4⟩. ⟨hal-00576948⟩