Room 206 (2nd floor, badged access)
12 March 2020 - 14h00
Updatable Parametric Timed Automata: Decidability, Algorithms, and Application to Security
by Mathias RAMPARISON from University of Luxemburg
Abstract: 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 system is 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.
We focus on the verification of timed concurrent
systems. Timed-dependent systems are very hard to verify, especially
when the exact value of timing constants remains unknown. These unknown
timing constants are called parameters. We study several subclasses of
a parametric 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)
