An Inverse Method for Parametric Timed Automata

Étienne André Emmanuelle Encrenaz 1 Laurent Fribourg Thomas Chatain 2, 3
1 ALSOC - Architecture et Logiciels pour Systèmes Embarqués sur Puce
LIP6 - Laboratoire d'Informatique de Paris 6
3 MEXICO - Modeling and Exploitation of Interaction and Concurrency
LSV - Laboratoire Spécification et Vérification [Cachan], ENS Cachan - École normale supérieure - Cachan, Inria Saclay - Ile de France, CNRS - Centre National de la Recherche Scientifique : UMR8643
Abstract : We consider in this paper systems modeled by timed automata. The timing bounds involved in the action guards and location invariants of our timed automata are not constants, but parameters. Those parametric timed automata allow the modelling of various kinds of timed systems, e.g. communication protocols or asynchronous circuits. We will also assume that we are given an initial tuple π0 of values for the parameters, which corresponds to values for which the system is known to behave properly. Our goal is to compute a constraint K0 on the parameters, satisfied by π0, guaranteeing that, under any parameter valuation satisfying K0, the system behaves in the same manner: for any two parameter valuations satisfying K0, the behaviors of the timed automata are (time-abstract) equivalent, i.e., the traces of execution viewed as alternating sequences of actions and locations are identical. We present an algorithm InverseMethod that terminates in the case of acyclic models, and discuss how to extend it in the cyclic case. We also explain how to combine our method with classical synthesis methods which are based on the avoidance of a given set of bad states. A prototype implementation has been done, and various experiments are described.
Type de document :
Article dans une revue
International Journal of Foundations of Computer Science, World Scientific Publishing, 2009, 20 (5), pp.819-836. 〈10.1142/S0129054109006905〉
Liste complète des métadonnées

https://hal.inria.fr/hal-00772641
Contributeur : Stefan Haar <>
Soumis le : jeudi 10 janvier 2013 - 20:32:45
Dernière modification le : jeudi 11 janvier 2018 - 06:27:10

Identifiants

Collections

Citation

Étienne André, Emmanuelle Encrenaz, Laurent Fribourg, Thomas Chatain. An Inverse Method for Parametric Timed Automata. International Journal of Foundations of Computer Science, World Scientific Publishing, 2009, 20 (5), pp.819-836. 〈10.1142/S0129054109006905〉. 〈hal-00772641〉

Partager

Métriques

Consultations de la notice

223