Jun 112014

The paper Organising LTL Monitors over Distributed Systems with a Global Clock has been accepted in RV 2014: the 14th International Conference on Runtime Verification, September 22 – September 25, 2014 Toronto, Canada.

Here is the abstract of the paper:

Users wanting to monitor distributed systems often prefer to abstract away the architecture of the system, allowing them to directly specify correctness properties on the global system behaviour. To support this abstraction, a compilation of the properties would not only involve the typical choice of monitoring algorithm, but also the organisation of submonitors across the component network. Existing approaches, considered in the context of LTL properties over distributed systems with a global clock, include the so-called orchestration and migration approaches. In the orchestration approach, a central monitor receives the events from all subsystems. In the migration approach, LTL formulae transfer themselves across subsystems to gather local information.

We propose a third way of organising submonitors: choreography — where monitors are orgnized as a tree across the distributed system, and each child feeds intermediate results to its parent. We formalise this approach, proving its correctness and worst case performance, and report on an empirical investigation comparing the three approaches on several concerns of decentralised monitoring.

This is joint work with Christian Colombo from University of Malta.

A pre-print of the paper can be downloaded here.


May 062014

The paper Enforcement and Validation (at runtime) of Various Notions of Opacity has been accepted to Discrete Event Dynamic Systems, a Springer journal. This is an extended version of our paper that appeared in CDC 2013. One of the new contributions of this paper is to introduce what we call K-step strong opacity.

The abstract of the paper is below.

We are interested in the validation of opacity. Opacity models the impossibility for an attacker to retrieve the value of a secret in a system of interest. Roughly speaking, ensuring opacity provides confidentiality of a secret on the system that must not leak to an attacker. More specifically, we study how we can model-check, verify and enforce at system runtime, several levels of opacity. Besides existing notions of opacity, we also introduce K-step strong opacity, a more practical notion of opacity that provides a stronger level of confidentiality.

A pre-print of the paper can be downloaded here.

This is joint work with Hervé Marchand, from Inria Rennes.

Mar 242014

This week I am attending SAC 2014, the 29th Symposium On Applied Computing, Gyeongju, Korea. I am also presenting our work with Inria Rennes on Runtime Enforcement of Regular Timed Properties.

edit: Here are the slides I have presented.

Mar 112014

The paper Efficient and Generalized Decentralized Monitoring of Regular Languages has been accepted to FORTE’14, the 34th IFIP International Conference on Formal Techniques for Distributed Objects, Components and Systems, June 3-6, 2014, Berlin, Germany.

Below is the abstract of the paper.

This paper proposes an efficient and generalized decentralized monitoring algorithm allowing to detect satisfaction or violation of any regular specification by local monitors alone in a system without central observation point. Our algorithm does not assume any form of synchronization between system events and communication of monitors, uses state machines as underlying mechanism for efficiency, and tries to keep the number and size of messages exchanged between monitors to a minimum. We provide a full implementation of the algorithm with an open-source benchmark to evaluate its efficiency in terms of number, size of exchanged messages, and delay induced by communication between monitors. Experimental results demonstrate the effectiveness of our algorithm which outperforms the previous most general one along several (new) monitoring metrics.

This is joint work with Tom Cornebize and Jean-Claude Fernandez, LIG and Verimag lab, Grenoble.

Mar 102014

This week I am visiting HUST – Hanoi University of Sciences and Technology (aka IPH – Institut Polytechnique de Hanoi) to work with Thanh Hung Nguyen.

Feb 122014
PERSYVAL-Lab and NASA-JPL are organizing the second edition of the CPS Summer School. The broad objective of the CPS Summer School is to explore the manifold relationship between networked embedded systems (« the internet of things ») and humans as their creators, users, and subjects. The format of the Summer School is a five days meeting, organized around different aspects of rigorous engineering of Cyber-Physical Systems.

This year, the objective of the school is to survey fundamental and applied aspects of modelling, monitoring and learning of systems as well as to identify novel opportunities and research directions in these areas through a series of lectures by international experts. Participants will also experience the relevant technologies during hands-on courses and be given a chance to present their own work. The school will provide a great opportunity to know other people working in the field, to meet distinguished scholars, and to establish contacts that may lead to research collaborations in the future.

The school will concentrate on the fields of system modelling, monitoring and learning. Over the last ten years we have seen a lot of growth in these areas, building on strong theoretical foundations to apply and extend techniques to new application domains. Runtime verification is a growing field with more and more efffective applications in safety/mission-critical systems, enterprise and systems software, autonomous and reactive control systems, health management and diagnosis systems, and system security and privacy. The field of specification mining (learning specifications from system behaviour) has also seen a surge in research effort, with the establishment of a number of competitions to drive forward the development of practical tools. This research community is at an ideal stage to benefit from a school such as this, to inspire, motivate and instruct new researchers into the field.

Students participating at this summer school will learn the current state of the art in modeling, monitoring, and learning. Students will be able to apply new techniques coming from various communities and backgrounds to their own domain. The CPS Summer School will be held at Grenoble University. Courses will be given in English by experts from industry and academia working in various fields of CPS.


• System modeling.
• Monitoring.
• Learning.
• Medical devices.
• Sensor networks.

Confirmed Speakers:

• Eric Bodden (TU Darmstadt and EC SPRIDE, Germany).
• Olivier Coutelou (Schneider Electric, France).
• Radu Grosu (Technical Univesity Wien, Austria).
• Jean Goubault-Larrecq (ENS Cachan, France).
• Klaus Havelund (NASA JPL, USA).
• Kim G. Larsen (Aalborg University, Denmark).
• Martin Leucker (University of Lübeck, Germany).
• Roberto Passerone (Universita’ degli Studi di Trento, Italy).
• Grigore Rosu (University of Illinois at Urbana Champaign, USA).
• Mohamad Sawan (Ecole Polytechnique de Montréal, Canada).
• Bernhard Steffen (Technical University Dortmund, Germany).
• Andreas Zeller (Saarland University, Germany).

Organization Committee:

• Saddek Bensalem – University of Grenoble, France.
• Yliès Falcone – University of Grenoble, France.
• Klaus Havelund – NASA JPL, USA.

Registration fee is €250 for students, €400 for non-students, which includes lunches and coffee breaks from Monday 8th through Thursday 11th, and a party. The registration fee only partially covers the costs incurred. The remaining costs are covered by PERSYVAL-Lab. The local organization committee has arranged university accommodations for students. Please refer to the Website for more details.

Application Procedure and Important Dates (please refer to the Website for the full procedure):

• Deadline for Application: April 14, 2014.
• Response to Applicants: April 21, 2014.
• Online Registration and Fee payment: May 10, 2014.
• Summer school on CPS: July 7-11, 2014.
Since attendance is limited, priority will be given to Ph.D. students and companies’ staff.More details can be found at: https://persyval-lab.org/en/summer-school/cps14.

Applications can be submitted at: https://persyval-calls.imag.fr/en/project/10.

Enquiries can be sent to cps-school.organization@imag.fr.

Jan 202014

This week I am visiting Laboratoire Bordelais de Recherche en Informatique (Bordeaux computer science research lab) to work with Antoine Rollet, Serge Chaumette, Hervé Marchand, and Srinivas Pinisetty.

Thank you Antoine for the invitation.