View article

We present an inverse method allowing to synthesize constraints on timing delays (seen as parameters) in the framework of timed automata. We take advantage of a given reference valuation of the parameters for which the system is known to behave properly, and we want to generalize this valuation. Our aim is to generate a constraint such that, under any valuation satisfying this constraint, the traces of the system (viewed as alternating sequences of locations and actions) are equivalent to the traces under the reference valuation. In particular, LTL formulas are preserved. This is useful for safely relaxing some values of the reference valuation. By iterating this inverse method on integer points of a rectangular parameter domain, we are then able to partition the parametric space into good and bad zones with respect to a given property on traces. A tool, IMITATOR, was developed and was successfully applied to …