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/