Le but ici est de vous faire expérimenter certaines subtilité de l’outil PRISM. Ce TP se terminera par un problème de modélisation « ouvert ». Dans ce cas, nous vous encourageons à discuter entre vous pour déterminer comment le modéliser.

I Problème ouvert :

Nous allons maintenant considérer comme modèle d’une réplique la situation suivante :

Chaque transition représente une exécution de la réplique :

si la destination de la transition est 1 alors l’exécution est considérée comme correcte

si la destination de la transition est 0 alors l’exécution de la réplique est défaillante mais transitoirement.

Dans ce cas la prochaine exécution sera aussi incorrecte avec probabilité 1 mais l’exécution d’après aura les mêmes probabilité et états de destination que les transition sortant de l’état correct (i..e a priori non défaillant).

Le système peut transiter vers l’état -1 qui est une défaillance permanente de ce dernier

Les probabilités de transition seront les suivantes : 1-> 1 : 0.99, 1->(0 :0.01- lambda) et 1->-1 : lambda.

Le but est de calculer

1. le nombre de répliques à déployer en réplication active pour garantir 10^-5 comme probabilité de défaillance en valeur du système au minimum pour les 100 premières exécutions (si l’on suppose que la défaillance d’état 0 est le cas byzantin, et -1 le crash).
2. le nombre de répliques à déployer en réplication active pour garantir 10^-9 comme probabilité de défaillance en valeur du système au minimum pour les 100 premières exécutions (si l’on suppose que la défaillance d’état 0 est le cas byzantin, et -1 le crash).
3. La valeur maximale de lambda permettant de garantir une disponibilité de 0.999 pour 100 exécution consécutive pour un modèle à 3 répliques (un modèle de récompense sera à définir dans ce cas)

II Si vous avez le temps : A propos de la synchronisation :

Nous allons partir du modèle ci dessous qui est définit à partir d’un produit de chaines de Markov:

dtmc 
const double rel;// rel = reliability
module rep1 
x1:[0..1] init 1 ; 
[] (x1=1)->rel: (x1'=x1)+ (1-rel):(x1'=0);
[] (x1=0)->1: (x1'=x1);
endmodule
module rep2=rep1[x1=x2] endmodule 
module rep3=rep1[x1=x3] endmodule 

La propriétés intéressante pour ce modèle est :

// probabilité de n'avoir jamais défailli jusque'à la date T
P=? [G<=T (x1+x2+x3>=2)]

Tracer cette probabilité pour T de 1 à 20, pourquoi à votre avis la probabilité à la date 1 d’avoir x1+x2+x3>=2 est de 1 ?

Indice regarder les supports de cours sur la partie produit synchronisé d’automate (rappel) la partie entre crochet est le nom des transitions (si pas de nom, un nom purement local est attribué).

Un ingénieur propose de tracer P=? [F[3*T,3*T] (x1+x2+x3>=2)] est ce que cela changerait quelque chose (serait ce correct) ? (justifiez)

Modifiez le modèle de sorte que P=? [F[T,T] (x1+x2+x3>=2)] capture la fiabilité du système au bout de T exécutions du système.

Nous souhaitons modéliser le fait qu’une réplique peut défaillir mais que cette défaillance peut à chaque nouvelle exécution être détectée et l’état du système réinitialisé à correct pour l’exécution suivante.