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.
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.