Treffer: On the theory and practice of updatable parametric timed automata ; Sur la théorie et l'application des automates paramétrés temporisés avec mises à jour

As cyber-physical systems become more and more complex, human debugging is not sufficient anymore to cover the huge range of possible behaviours. For costly critical systems where human lives can be endangered, formally proving the safety of a systemis even more crucial. This is done by defining a formal specification for the system, and then performing the algorithmic verification that the system satisfies some formally specified properties. With this precise and exhaustive description of a system, the usual vagueness of human language is eliminated. In this thesis, we focus on the verification of timed concurrent systems. Time-dependent systems are very hard toverify, especially when the exact value of timing constants remains unknown. Theseunknown timing constants are called parameters. We study several subclasses of aparametric extension of the well-known formalism called Timed Automata. We mainly focus on the reachability decision problem, that asks whether there exists concrete values for these parameters such that a bug state can be reached in the system. We further address for these subclasses a computation problem that is to synthesise the set of parameter values for which a state is reachable. Finally, we apply our work to the security and safety of cyber-physical systems and infrastructure : we extend with parameters a classic formalism to model attack and failure scenarios called attack-fault trees, and propose an implementation of the translation of parametric attack-fault trees to parametric timed automata. This allows us to leverage the verification techniques and tools available for the latter for the analysis of (parametric) attack-fault trees. ; A mesure que les systèmes cyber-physiques deviennent de plus en plus complexes,le débogage humain ne suffit plus pour analyser le grand nombre de comportements possibles. Pour les systèmes critiques coûteux où des vies humaines peuvent être mise sen danger, il est encore plus crucial de prouver formellement la sécurité d'un système.Pour ce faire, on ...