commande à saisir pour pouvoir lancer directement xprism :
export PATH=/cal/homes/trobert/tool/prism-4.3-linux64/bin/:$PATH
Dans ce tp nous allons reprendre un modèle similaire à celui du tp précédant. Le modèle décrit un calculateur pour lequel le calculateur a trois fonctionnements possibles:
- le cas normal : état 1;
- le cas défaillance en valeur : état 0; Attention le sens des valeurs a changé peut être !
- le cas défaillance par crash : état -1;
dtmc
const double def_V = 0.1; // probabilité d’une défaillance en valeur
const double def_C = 0.15; // probabilité d’une défaillance par crash.module myreplica1
x : [-1..1] init 1; //cf sens défini ci dessus
[](x=1) -> def_V: (x’=0) +def_C:(x’=-1) +1-(def_C+def_V):(x’=x);
[](x=0) -> def_C:(x’=-1) +def_V:(x’=x) + 1-(def_V +def_C):(x’=1);
[](x=-1)-> 1:(x’=x);
endmodule
Question 1 En supposant que chaque transition franchie correspond à une requête émise au calculateur : tracer l’évolution de la probabilité d’être dans l’état 1 depuis l’instant 0 jusqu’à la date t, puis la probabilité d’être dans l’état -1 à l’instant t ?
remarque : le but ici est de calculer la probabilité à la date t d’être resté dans l’état 1 (fiabilité), ou d’être dans l’état 1 à la date 1. Ce ne sont donc pas les mêmes formules qui faudra utiliser pour tracer ces probabilités.
Nous allons maintenant évaluer la probabilité de produire une résultat correct pour une architecture de réplication active à 3 répliques. Pour cela, nous allons étendre le modèle PRISM.
Il est possible
1 de créer une copie d’une chaine de markov, puis de remplacer les noms des variables d’état par substitution de texte. (explications ici)
2 d’analyser un « réseau de modules », le système réalise le produit synchronisé des automates correspondants. Si les transitions ne sont pas nommées : elles sont indépendantes (une « exécution » devient un entrelacement de transitions
Consigne :
- Ajoutez après « endmodule » :
module myreplica2= myreplica1[x=y] endmodule
module myreplica3= myreplica1[x=z] endmodule - Avant de synchroniser les modèles, utiliser le simulateur pour visualiser une « exécution du réseau de chaîne. Notez que seul une chaîne peut changer d’état à chaque fois. Utilisez un événement de synchronisation pour remédier à ce problème de modélisation
- Synchronisez les transitions de toutes les répliques de telles sorte que chaque fois qu’une réplique franchit une transition, chaque réplique franchit exactement une transition (tout le monde « avance » d’une exécution, aide : utilisez une transition synchronisée).
- évaluez la probabilité que 2 répliques parmi trois soient fonctionnelles au bout d’un « run », puis au bout de 10 exécutions ?
(vous pouvez le faire en calculant la somme des probabilité des états transitoires où 2 états sont fonctionnels, ou en écrivant une formule logique). ( commençant par exemple par » P=?[G<=1 « , puis utilisez l’opérateur G[T,T] avec T un paramètre ).
Question 2 : Calculez la fiabilité de cette architecture à la date 1 (après une exécution). Comparez la à celle d’une réplique.
Question 3 : Tracez l’évolution de la fiabilité en fonction du nombre d’exécutions consécutives pour la réplication et pour une réplique sur le même graphe.
Modifiez le modèle de sorte que la défaillance par crash ne se produise jamais. Conservez les mêmes probabilité de défaillance en valeur et adaptez les autres transitions.
Question 4 : Tracer l’évolution au cours du temps de la fiabilité et de la disponibilité de cette architecture. (Y a t il une différence entre les deux concepts ?), on suppose le voteur élémentaire si le nombre de réponses identiques est de 2 au moins, un résultat est produit (les défaillances en valeur sont à considérer comme malicieuses par exemple).
Question 5 Ajoutez un nouveau module permettant de modélisant l’ajout de calculateur de rechange en nombre borné permettant de faire passer un calculateur crashé à l’état 1 si il reste des ressources.