Exemplifying Parametric Timed Specifications over Signals with Bounded Behavior
Résumé
Specifying properties can be challenging work.
In this paper, we propose an automated approach to exemplify properties given in the form of automata extended with timing constraints and timing parameters, and that can also encode constraints over real-valued signals.
That is, given such a property and given an admissible automaton for each signal, we output concrete runs exemplifying real (or impossible) runs for this property.
Specifically, our method takes as input a property, and a set of admissible behaviors, all given as a subclass of linear hybrid automata, namely timed automata extended with arbitrary clock rates and timing parameters.
Our method then generates concrete runs exemplifying the property.