Séminaires
Séminaire du 16 Décembre 2011
Lieu
CNAM, salle 30.-1.05: comment y aller
Programme
14h00-15h00: L. Hillah, LIP6 - UPMC "Standardisation of Petri Nets: a DSML approach for semantic, syntactic extensibility and executability"
Abstract: 
The ongoing standardisation effort on Petri Nets (ISO/IEC 15909) to set up a unifying framework for their defition and syntactic extensibility has reached a crossroads. Promising results in recent experimentations on extending PNML scope, semantically and syntactically, showed that the extension framework we are trying to build could be further extended and enhanced. In particular, the mechanisms for syntactic extensions and for the corresponding semantic mappings in the standardisation context brought up issues the community has not dealt with before.
Morever, recent work on structuring mechanisms and executability we will highlight in this talk underline the need for a DSML framework. We will sketch this framework, from a state-of-the-art perspective and provide insights into how the WG19 Petri Nets subgroup is handling these latest developments. These developments rely on contributions provided these last few months by Petri Nets experts from Australia, France, Germany and Switzerland.
The expected benefit is a more open and flexible standardised framework for the Petri Nets community. This framework will allow building more compatible model-based platforms for model transformation, executability and traceability.
Finally, we will also give an update of the current standardisation process and show the the preliminary tables of contents for Part 1 and Part 3 in which will be shaped the above mentioned contributions.
15h00-15h30 : R. Abo, CEDRIC/CNAM, "Approches formelles pour l'analyse de la performabilité des systmes communicants mobiles"
Abstract: Nous nous intéressons à l'analyse formelle de la performabilité des systèmes communicants mobiles. Nous modélisons ces systèmes à l'aide d'un formalisme de haut niveau issu du pi-calcul permettant de spécifier des comportements stochastiques, temporels, déterministes ou indéterministes. Ce formalisme est ensuite étendu après avoir traduit la communication par diffusion en termes du pi-calcul. Afin de pallier à l'absence d'outils d'analyse des propriétés des modèles spécifiés en pi-calcul, nous avons établi des règles de traduction en langage Prism permettant ainsi de traduire nos modèles de haut niveau spécifiés en pi-calcul étendu, en modèles de bas niveau supportés par l'outil Prism, tels que des chaînes de Markov à temps discret, à temps continu ou des automates temporisés probabilistes. Nous illustrons notre approche à travers l'analyse de la performabilité d'un réseau de capteurs sans fil mobiles déployé dans un hôpital.