Today at 1:30pm, Srinivas Pinisetty will defend his Ph.D. thesis on Runtime Enforcement of Timed Properties at Inria Rennes, Salle Métivier.
Jury:
- Martin LEUCKER
- Didier LIME
- Sophie PINCHINAT
- Frédéric HERBRETEAU
- Yliès FALCONE
- Thierry JÉRON
- Hervé MARCHAND
Here is the abstract of the thesis:
Runtime enforcement is a verification/validation technique aiming at correcting possibly incorrect executions of a system of interest. It is a powerful technique to ensure that a running system satisfies some desired properties. Using an enforcement monitor, an (untrustworthy) input execution (in the form of a sequence of events) is modified into an output sequence that complies with a property. Over the last decade, runtime enforcement has been mainly studied in the context of untimed properties.
In this thesis, we consider enforcement monitoring for systems where the physical time elapsing between actions matters. Executions are thus modeled as sequences of events composed of actions with dates (called timed words). We consider runtime enforcement for timed specifications modeled as timed automata, in the general case of regular timed properties. The proposed enforcement mechanism has the power of both delaying events to match timing constraints, and suppressing events when no delaying is appropriate, thus allowing the enforcement mechanisms and systems to continue executing.
To ease their design and correctness-proof, enforcement mechanisms are described at several levels: enforcement functions that specify the input-output behavior in terms of transformations of timed words, constraints that should be satisfied by such functions, enforcement monitors that describe the operational behavior of enforcement functions, and enforcement algorithms that describe the implementation of enforcement monitors. The feasibility of enforcement monitoring for timed properties is validated by prototyping the synthesis of enforcement monitors from timed automata. We also show the usefulness of enforcement monitoring of timed specifications for several application-domains.
I have unofficially supervised Srinivas’ Ph.D. thesis and we actively collaborated during the three years of his Ph.D. work.
Edit: