Evènement pour le groupe Modélisation et Verification


Date 2010-12-09  11:30-12:45
TitreWhat Can You Verify and Enforce at Runtime ? 
RésuméRuntime verification is an effective technique to ensure at execution time that a system meets a desirable behavior. It can be used in numerous application domains, and more particularly when integrating together untrusted software components. In runtime verification, a run of the system under scrutiny is analyzed incrementally using a decision procedure: a monitor. This monitor may be generated from a user-provided high level specification (e.g. a temporal property, an automaton). Runtime enforcement is an extension of runtime verification aiming to circumvent property violations. In runtime enforcement the monitors watch the current execution sequence and modify the execution sequence of the underlying program whenever it deviates from the desired property. More than simply halting an underlying program, some enforcement mechanisms can also ``suppress'' (i.e. freeze) and ``insert'' (frozen) actions in the current execution sequence. Runtime verification and enforcement have proved to be effective techniques to achieve software reliability. The questions we consider in this talk are the following: what are the classes of properties that can be verified and enforced at runtime, and is there a difference between the techniques we are interested in? These questions are not new, but we propose here to address them within a unified framework: the Safety-Progress classification of properties introduced by Manna and Pnueli. In this talk, we start first by customizing the Safety-Progress classification in a runtime verification and enforcement context. Then we revisit the existing classical definition of monitorability, and characterize the set of monitorable properties according to this definition. Then, we parameterize this definition according to the truth-domain under consideration. Moreover, we introduce a new definition of monitorability based on distinguishability of ``good'' and ``bad'' execution sequences. This definition is weaker than the classical one, but we believe that it better corresponds to practical needs and tool implementations. Furthermore, we characterize the set of enforceable properties in a way that is independent from any enforcement mechanism. A consequence is that the proposed set of enforceable properties is an upper bound of any enforcement mechanism. This is joint work with Pr. Jean-Claude Fernandez and Dr. Laurent Mounier from Vérimag (Grenoble).  
LieuSalle 076, LaBRI, Rez-de-chaussée 
OrateurYlies Falcone  
Emailylies.falcone@inria.fr 
Urlprojet VERTECS/INRIA, Rennes 



Aucun document lié à cet événement.

Retour
Retour à l'index