**Date: **
Thursday, December 02, 2010

**Speaker: **
<a href = "http://www.lsv.ens-cachan.fr/~andre/"> Etienne Andre </a>

**Venue: **TU Wien

I will present an inverse method allowing to synthesizeconstraints on timing delays (seen as parameters) in theframework of timed automata.Given a reference valuation of the parameters, this method synthesizesa constraint on the parameters, guaranteeing the sametime-abstract linear behavior as for the referencevaluation.This is useful for safely relaxing some values of the referencevaluation and gives a criterion of robustness to the system.In particular, LTL formulae are preserved.By iterating this inverse method on various points of a boundedparameter domain, we are then able to partition theparametric space into good and bad zones, with respect to agiven property one wants to verify.A tool, IMITATOR, was developed and was successfully applied tovarious examples of asynchronous circuits and protocols.An extension to probabilistic timed systems allows to synthesize aconstraint on the timing parameters guarantying the value ofthe reachability probabilities.