Organized by: 
Danielle Ziebelin
Yliès Falcone

13 December 2012, 12:00 - 13:00 
Le Pulsar - 4 av du Doyen Louis Weil 38000 GRENOBLE

Yliès Falcone received the Master degree (2006) and PhD (2009) in computer science from the University of Grenoble at Verimag Laboratory. His research interests concern formal runtime validation techniques for various application domains, i.e. techniques aiming at evaluating whether a system meets a set of desired properties during its execution. He has been a member of the organization committee of CAV’09, RV’10 and IsoLA’12. He usually serves as a program committee member of the Runtime Verification conference. Since September 2011, he is an associate professor at University of Grenoble and a researcher at Laboratory of Informatics Grenoble. From December 2009 to August 2011, he has been a postdoctoral researcher at INRIA Rennes in the VerTeCs project. He has been an invited researcher in several places such as NASA JPL in Pasadena, NICTA Canberra, Manchester University and University of Illinois.

In this talk, I will present some recent results on the topic of monitoring. The first part of this talk presents a solution for monitoring distributed systems. The second part of this presents what the techniques of runtime monitoring allow when trying to improve the security, safety and reliability of Android applications.

- Part 1 : Decentralized LTL Monitoring

Users wanting to monitor distributed or component-based systems often perceive them as monolithic systems which, seen from the outside, exhibit a uniform behavior as opposed to many components displaying many local behaviors that together constitute the system’s global behavior. This level of abstraction is often reasonable, hiding implementation details from users who may want to specify the system’s global behavior in terms of an LTL formula. However, the problem that arises then is how such a specification can actually be monitored in a distributed system that has no central data collection point, where all the components’ local behaviors are observable.

- Part 2 : Runtime Verification and Enforcement for Android Applications with RV-Droid

RV-Droid is an implemented framework dedicated to runtime verification (RV) and runtime enforcement (RE) of Android applications. RV-Droid consists of an Android application that interacts closely with a cloud. Running RV-Droid on their devices, users can select targeted Android applications from Google Play (or a dedicated repository) and a property. RV-Droid is generic and currently works with two existing runtime verification frameworks for (pure) Java programs : with Java- MOP and (partially) with RuleR. RV-Droid does not require any modification to the Android kernel and targeted applications can be retrieved off-the-shelf. We carried out several experiments that demonstrated the effectiveness of RV-Droid on monitoring (security) properties.