HMSCs en tant que spécifications partielles et leurs complétions dans les réseaux de Petri

Benoit Caillaud 1 Philippe Darondeau 2 Loïc Hélouët 1 Gilles Lesventes 2
1 PAMPA - Models and Tools for Programming Distributed Parallel Architectures
IRISA - Institut de Recherche en Informatique et Systèmes Aléatoires, INRIA Rennes
2 PARAGRAPHE - Parallelism and Graphs
IRISA - Institut de Recherche en Informatique et Systèmes Aléatoires, INRIA Rennes
Résumé : Nous présentons les premiers résultats d'une étude visant à comprendre la nature des spécifications données par des HMSCs (High Level Message Sequence Charts) et les modalités de leur utilisation pratique. Contrairement à d'autres auteurs, nous n'imposons aux HMSCs aucune restriction de type fini, afin d'adhérer au mieux au style des systèmes distribués qui voient le jour dans le domaine des télécommunications. Nous donnons d'abord une série de résultats d'indécidabilité sur les HMSCs, établis par réduction de résultats d'indécidabilité sur les sous-ensembles rationnels de monoïdes produits. Ces résultats négatifs ne sont pas surprenants mais ils n'apparaissent pas à notre connaissance dans la littérature sur les HMSCs. Ces résultats indiquent clairement que le seul angle sous lequel on peut raisonnablement considérer et utiliser les HMSCs comme des spécifications de comportements est d'interpréter leurs extensions linéaires comme des langages minimaux à approximer supérieurement dans toute réalisation. Le problème est alors de rechercher un cadre dans lequel on puisse donner une signification précise à ces spécifications incomplètes au moyen d'une opération de fermeture. La seconde partie du rapport étudie la fermeture des langages de HMSCs dans les langages de réseaux de Petri. Cette opération de fermeture correspond à une procédure effective, reposant sur la semi-linéarité des images commutatives des langages de HMSCs. Nous présentons pour finir quelques résultats effectifs afférents à la répartition et à la vérification automatisées des réalisations de HMSCs par des réseaux de Petri.
Type de document :
Rapport
[Rapport de recherche] RR-3970, INRIA. 2000
Liste complète des métadonnées

https://hal.inria.fr/inria-00072678
Contributeur : Rapport de Recherche Inria <>
Soumis le : mercredi 24 mai 2006 - 10:33:52
Dernière modification le : jeudi 11 janvier 2018 - 06:20:09
Document(s) archivé(s) le : dimanche 4 avril 2010 - 23:18:05

Fichiers

Identifiants

  • HAL Id : inria-00072678, version 1

Collections

Citation

Benoit Caillaud, Philippe Darondeau, Loïc Hélouët, Gilles Lesventes. HMSCs en tant que spécifications partielles et leurs complétions dans les réseaux de Petri. [Rapport de recherche] RR-3970, INRIA. 2000. 〈inria-00072678〉

Partager

Métriques

Consultations de la notice

186

Téléchargements de fichiers

126