Skip to Main content Skip to Navigation
Reports

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.
Document type :
Reports
Complete list of metadata

https://hal.inria.fr/inria-00072678
Contributor : Rapport de Recherche Inria <>
Submitted on : Wednesday, May 24, 2006 - 10:33:52 AM
Last modification on : Thursday, February 11, 2021 - 2:48:04 PM
Long-term archiving on: : Sunday, April 4, 2010 - 11:18:05 PM

Identifiers

  • HAL Id : inria-00072678, version 1

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⟩

Share

Metrics

Record views

247

Files downloads

180