Nous utilisons les réseaux de Petri contextuels avec arcs inhibiteurs pour exprimer la sémantique opérationnelle d'un langage de coordination de type Linda, Ce langage utilisant la composition alternative, la sémantique que nous proposons est orientée-location. Nous adoptons une vue statique du comportement d'un agent afin de limiter le nombre des places dans les réseaux. Nous montrons ensuite que la sémantique ainsi exprimée est équivalente à celle décrite dans le style de Plotkin. Nous proposons également une application qui génère le fichier de réseaux qui est traité par un outil d'analyse et de vérification des propriétés de réseaux de Petri, INA.
Sémantique et vérification de langages de coordination par les réseaux de Petri
Mayala Lusilabo mfumua'Nsi, F. (Auteur). 2005
Student thesis: DEA types › DEA en Informatique