CTL
9 November 2009 - 14h00
Study and implementation of runtime validation techniques (Phd Defense)
by Yliès Falcone from Vérimag
Abstract: This thesis deals with three dynamic validation techniques: runtime verification (monitoring), runtime enforcement, and testing from property. We consider these approaches in the absence of complete behavioral specification of the system under scrutiny. Our study is done in the context of the Safety-Progress classification of properties. This framework offers several advantages for specifying properties on systems. We adapt the results on this classification, initially dedicated to infinite sequences, to take into account finite sequences. Those sequences may be considered as abstract representations of a system execution. Relying on this general framework, we study the applicability of dynamic validation methods. We characterize the classes of monitorable, enforceable, and testable properties. Then, we proposed three generic approaches for runtime verification, enforcement, and testing. We show how it is possible to obtain, from a property expressed in the Safety-Progress framework, some verification, enforcement, and testing mechanisms for the property under consideration. Finally, we propose the tools j-VETO and j-POST implementing all the aforementioned results on Java programs.
Jury composé de :
- Klaus Havelund (SRS @ JPL, NASA, USA), Rapporteur
- Thierry Jéron (DR @ IRISA -- INRIA de Rennes), Rapporteur
- Howard Barringer (PR @ Manchester University), Examinateur
- Ahmed Bouajjani (PR @ Université de Paris 7), Éxaminateur
- Jean-François Méhaut (PR @ Université Joseph Fourier), Éxaminateur
- Jean-Claude Fernandez (PR @ Université Joseph Fourier), Directeur
- Laurent Mounier (MCF @ Université Joseph Fourier), Co-Directeur
- Jean-Luc Richier (CR @ LIG), Co-Directeur
