salle A. Turing CE4
28 avril 2016 - 14h00
Parallel, distributed behavioral cartography of parametric timed automata
par Camille Coti de Université Paris XIII / LIPN
Abstract: Parametric timed automata (PTA) allow the specification and verification of timed systems incompletely specified, or subject to future changes. The behavioral cartography splits the parameter space of PTA in tiles in which the discrete behavior is uniform. Applications include the optimization of timing constants, and the measure of the system robustness w.r.t. the untimed language. I will present a set of parallel algorithms and domain decomposition heuristics to compute the cartography efficiently, and experimental results to compare their performance.