Avoiding Shared Clocks in Networks of Timed Automata - Inria - Institut national de recherche en sciences et technologies du numérique Accéder directement au contenu
Rapport (Rapport De Recherche) Année : 2012

Avoiding Shared Clocks in Networks of Timed Automata

Résumé

Networks of timed automata (NTA) are widely used to model distributed real-time systems. Quite often in the literature, the automata are allowed to share clocks, i.e. the transitions of one automaton may be guarded by a condition on the value of clocks reset by another automaton. This is a problem when one considers implementing such model in a distributed architecture, since reading clocks a priori requires communications which are not explicitly described in the model. We focus on the following question: given a NTA A1 || A2 where A2 reads some clocks reset by A1, does there exist a NTA A'1 || A'2 without shared clocks with the same behavior as the initial NTA? For this, we allow the automata to exchange information during synchronizations only, in particular by copying the value of their neighbor's clocks. We discuss a formalization of the problem and give a criterion using the notion of contextual timed transition system, which represents the behavior of A2 when in parallel with A1. Finally, we effectively build A'1 || A'2 when it exists.
Les réseaux d'automates temporisés sont largement utilisés dans la modélisation des systèmes temps-réel distribués. Le plus souvent dans la littérature, le partage d'horloges entre les différents automates est autorisé : les transitions d'un automate peuvent être conditionnées par la valeur d'horloges remises à zéro par un autre automate. Cela pose problème lorsque l'on envisage l'implantation d'un tel modèle sur une architecture distribuée, puisque la lecture des horloges requiert a priori des communications qui ne sont pas décrites explicitement dans le modèle. Nous nous intéressons à la question suivante : étant donné un réseau d'automates temporisés A1 || A2 où A2 lit des horloges remises à zéro par A1 , existe-t-il un réseau d'automates temporisés A'1 || A'2 sans horloges partagées avec le même comportement que le réseau initial ? Dans cette optique, nous autorisons les automates à échanger de l'information pendant les synchronisations seulement, en copiant les valeurs des horloges de leur voisin. Nous discutons d'abord d'une formalisation de ce problème, puis nous donnons un critère pour décider de l'existence du système sans horloges partagées, en introduisant la notion de système de transition temporisé contextuel. Ce système de transition représente le comportement de A2 lorsqu'il est en parallèle avec A1. En fin, nous montrons comment construire A'1 || A'2 quand il existe.
Fichier principal
Vignette du fichier
RR-7990.pdf (495.63 Ko) Télécharger le fichier
Origine : Fichiers produits par l'(les) auteur(s)
Loading...

Dates et versions

hal-00706608 , version 1 (11-06-2012)

Identifiants

  • HAL Id : hal-00706608 , version 1

Citer

Sandie Balaguer, Thomas Chatain. Avoiding Shared Clocks in Networks of Timed Automata. [Research Report] RR-7990, INRIA. 2012, pp.26. ⟨hal-00706608⟩
134 Consultations
130 Téléchargements

Partager

Gmail Facebook X LinkedIn More