LRDE: plans d'accès ici et ici.
Abstract: For a large Markovian model, a "product form" is an explicit   description of the steady-state behaviour which is otherwise   generally untractable. Being first introduced in queueing networks,   it has been adapted to Markovian Petri nets. Here we address three   relevant issues for product-form Petri nets which were left fully or   partially open: (1) we provide a sound and complete set of rules for   the synthesis; (2) we characterise the exact complexity of classical   problems like reachability; (3) we introduce a new subclass for   which the normalising constant (a crucial value for product-form   expression) can be efficiently computed.
For a large Markovian model, a "product form" is an explicit   description of the steady-state behaviour which is otherwise   generally untractable. Being first introduced in queueing networks,   it has been adapted to Markovian Petri nets. Here we address three   relevant issues for product-form Petri nets which were left fully or   partially open: (1) we provide a sound and complete set of rules for   the synthesis; (2) we characterise the exact complexity of classical   problems like reachability; (3) we introduce a new subclass for   which the normalising constant (a crucial value for product-form   expression) can be efficiently computed.
Abstract: Dans un système de stockage de données distribué, la disponibilité des données est une propriété critique à assurer. Pour analyser la robustesse du système de stockage UbiStorage on a procédé à l'évaluation de ce dernier en présence d'attaquants internes en utilisant la simulation. Pour résoudre le problème de perte de données ainsi détecté, un système de réputation est mis en place. Dans cet exposé, nous allons voir l'utilisation du formalisme ABCD pour la modélisation du système de stockage pair-à-pair d'UbiStorage et la modélisation des différentes attaques ainsi que du système de notation. Nous allons aussi voir les résultats d'analyse par model-checking du système de notation.