Avoiding Shared Clocks in Networks of Timed Automata

Sandie Balaguer 1, 2, * Thomas Chatain 1, 2
* Auteur correspondant
2 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
Résumé : 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.
Type de document :
Rapport
[Research Report] RR-7990, INRIA. 2012, pp.26
Liste complète des métadonnées

Littérature citée [28 références]  Voir  Masquer  Télécharger

https://hal.inria.fr/hal-00706608
Contributeur : Sandie Balaguer <>
Soumis le : lundi 11 juin 2012 - 10:55:48
Dernière modification le : jeudi 11 janvier 2018 - 06:23:37
Document(s) archivé(s) le : mercredi 12 septembre 2012 - 02:25:35

Fichiers

RR-7990.pdf
Fichiers produits par l'(les) auteur(s)

Identifiants

  • HAL Id : hal-00706608, version 1

Collections

Citation

Sandie Balaguer, Thomas Chatain. Avoiding Shared Clocks in Networks of Timed Automata. [Research Report] RR-7990, INRIA. 2012, pp.26. 〈hal-00706608〉

Partager

Métriques

Consultations de la notice

235

Téléchargements de fichiers

138