[Apologies for multiple copies]

Dear all,

Let me advertise our next ERATO MMSD project colloquium talk by Étienne André and Bart Jacobs on 1 March, 16:00-. Please find the title and the abstract below. You are all invited.

Sincerely, -- Natsuki Urabe [email protected] The University of Tokyo, ERATO MMSD

----

Thu 1 March 2018, 16:00–18:00

ERATO MMSD Takebashi Site Common Room 3 http://group-mmm.org/eratommsd/access.html

16:00–17:00

Étienne André (University Paris 13), Parametric timed automata: theory and applications

Critical real-time systems must be formally verified to prevent any undesired behavior. When some timing constants are known with only a limited precision, traditional timed model-checking techniques may not apply anymore.

We use here the formalism of parametric timed automata. Parametric timed automata are very expressive, and decision problems are notoriously very hard (in fact most interesting decision problems are undecidable). On the one hand, we review decidability results, and propose new decidable subclasses. On the other hand, we adopt a more pragmatic approach, and show that parametric timed automata allow us to model and verify distributed real-time systems; using the IMITATOR software, we derive best- and worst-case execution times for a real-time system designed by Thales, and subject to uncertainty in some tasks periods.

We also briefly report on recent techniques to speed-up the verification time using abstractions, and on distributed parametric model checking.

17:00–18:00

Bart Jacobs (Radboud University), Privacy and Security in Identity Management and Medical Research

This talk will given an overview of the ideas behind two practically oriented security and privacy projects at Nijmegen, NL:

1. Attribute-based identity management via the IRMA platform, see https://privacybydesign.foundation/en/

If interested, you can before the talk already install the IRMA app on your (Android or iOS) phone and collect some attributes yourself. 2. Polymorphic encryption and Pseudonymisation for a large scale Parkinson research study, see: https://pep.cs.ru.nl/