|What Can You Verify and Enforce at Runtime ?|
du groupe Modélisation et Verification
|Date|| 2010-12-09 11:30-12:45|
|Titre||What 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).
|Lieu||Salle 076, LaBRI, Rez-de-chaussée |
|Orateur||Ylies Falcone |
|Url||projet VERTECS/INRIA, Rennes |
Aucun document lié à cet événement.RetourRetour à l'index