Auteur : Thomas Robert, relectures Kristen Vanhulst.
Exercice 1
Question 1
Le modèle proposé repose sur le principe que chaque arc franchi modélise l’exécution d’une réplique. Si cette exécution correspond à l’activation d’une faute, cela fait décroitre le nombre de répliques fonctionnelles (cas s’=s-1).
Ainsi, pour analyser la fiabilité de TMR suite à une exécution il est correct d’étudier la probabilité d’être dans l’état 2 ou 3 à l’instant 3 lorsque s vaut 3 dans l’état initial (i..e franchir 3 arcs correspond à atteindre un état où s représente le nombre de répliques fonctionnelles dans TMR suite à une exécution de TMR).
Par analyse de l’état transitoire, on trouve les probabilités de s=2 et s=3 qui au total correspondent à 0,84375.
Question 2
la formule cherchée est P=? [F[3,3] (s>= 2)]
Question 3
Exercice 2
Remarque sur le produit synchronisé: il faut comprendre le modèle d’écoulement du temps et la façon dans les probabilités ou les taux placés sur les transitions sont interprétés. PRISM construit le système à transition « produit » des modules déclarés de sorte à n’avoir qu’un seul système à transitions à traiter.
Les arcs synchronisés sont particuliers car leurs taux ou probabilités s’obtiennent en réalisant le produit des valeurs définies sur les arcs à synchroniser dans chaque modules (e.g. des probabilités en discret et des taux en continu). Ce produit peut avoir un sens pour les chaines discrètes. C’est assez délicat à manipuler en continu car le taux caractérise les dates de saut qui a priori sont des variables indépendantes. Il faut donc comprendre qu’en synchronisant les arcs vous rompez cette hypothèse d’indépendance des dates de saut(peut importe l’état de destination). La synchronisation force ces dates à être les mêmes pour les modules synchronisés sur un arc. Une unique transition modélisera ce changement d’état global et son taux sera défini comme le produit des taux de transition. L4inte’prétation pratique d’un tel produit est complexe. Ainsi si vous manipulez des taux >1, la transition arrivera « plus tôt » et sinon « plus tard » par rapport à des transitions jugées indépendantes. Pour ces raisons, dans le cas discret nous utiliserons le produit synchronisé (car l’énumération des chemin nous donnera bien une sémantique facilement interprétable). En revanche, dans le cas continu, tant que nous considérerons que les dates de changement d’état sont indépendantes, alors les modules ne devront pas être synchronisés.
Question 1
Supposons que l’état du processus étudié est noté \((s_k)_{k\ge 0}\). Les probabilité demandées sont des probabilités constantes grâce à la propriété de markov du processus.
L’expression 3-s correspond au nombre de répliques défaillantes à un instant donné. Nous vous demandons donc les probabilités conditionnelles suivantes pour n=0..3 :\(Cp_n=P(s_{k+1}\ge 2 |(3-s_k)=n)\).
Dans le sujet on note f la probabilité de défaillance
Le cas 0 correspond à une exécution de TMR depuis un état initial totalement fonctionnel, on retrouve la formule donnée dans l’exercice 1.
$$Cp_0=P(s_{k+1}\ge 2 |(3-s_k)=0)= (1-f)^3+ 3 *(1-f)^2*f$$
Le cas n=1 correspond au cas où une réplique est déjà défaillante. Il faut donc que les deux restantes ne subissent aucune activation de faute.
$$Cp_1=P(s_{k+1}\ge 2 |(3-s_k)=1)= (1-f)^2$$
Les deux derniers cas sont triviaux, les probabilité sont nulles car il y a trop de répliques défaillantes au départ (et pas de réparation).
Question 2
En utilisant les probabilités conditionnelles. On peut reformuler l’événement « 2 exécutions consécutives de TMR fiables à partir de l’état initial 3 répliques fonctionnelles » en une disjonction de deux événements disjoints :
Cas 1 : les trois répliques sont fonctionnelles à l’issue de la première exécution et la deuxième de TMRexécution reste fiable. La probabilité de cet événement est : $$(1-f)^3 * Cp_0$$
Cas_2 : exactement deux répliques parmi 3 sont fonctionnelles à l’issue de la première exécution de TMR et ces deux répliques le restent dans la seconde exécution : $$\left(3*(1-f)^2*f\right )*Cp_1$$
La somme de ces deux formules pour f=0.75 donne environ 0.59.
En revanche, la formule P=?[F[6,6] (s>=2)] donne 0.54. Ceci vient du fait que dans le modèle de l’exercice 1, nous ne pouvons pas distinguer le cas 1 du cas 2. Or pour obtenir la probabilité du cas 2 il ne faudrait ne considérer que 5 transitions… Ceci nous amène au constat que le problème prend son origine dans le modèle : dans l’état s=2 la probabilité de transition vers s=2 devrait tenir compte du fait que pour la réplique déjà défaillante la probabilité de laisser s invariant est de 1. Ce n’est pas le cas.
Question 4
Une version corrigée de la modélisation de la fiabilité de TMR serait :
dtmc
const double r;
module replica1x1 :[0..1] init 1 ;
[execute]x1=1 -> r :(x1’=1)+(1-r):(x1’=0);
[execute]x1=0 -> 1: (x1’=0);
endmodulemodule replica2 = replica1[x1=x2] endmodule
module replica3 = replica1[x1=x3] endmodule
On notera l’usage de la duplication de module avec les règles de substitution au format « [old=new] » qui remplace le texte old par new dans le module dupliqué. On notera par exemple qu’il est tout à fait possible dans ces conditions de définir des répliques qui ont des probabilités de défaillance différentes.
Question 5
La formule attendue est P=?[G[0,10] (x1+x2+x3>=2)] ou P=?[G[1,10] (x1+x2+x3>=2)]
Question 6
Réponse fournie dans le sujet …
Exercice 3
Question 1
Rappel :
Le taux d’une Variable V de loi \(exponentielle(\lambda)\) : \(\lambda= 1/E(V)\) avec E(V) l’espérance de la variable.
ctmc
const double lambda=1.0/(100*60);
module replica
state: [0..1] init 1;
[] state=1 -> lambda :(state’=0) ;
endmodule
Question 2
Ici vous devriez constater un léger écart et obtenir une valeur moyenne légèrement inférieur à 6000.
Question 2 bis
Le modèle demandé est le suivant :
ctmc const double lambda=1.0/(100*60); module replica1 state1: [0..1] init 1; [] state1=1 -> lambda :(state1'=0) ; endmodule module replica2 = replica1[state1=state2] endmodule module replica2 = replica1[state1=state2] endmodule
On notera que cette fois les transitions ne sont pas synchronisées. En effet, l’état de chaque calculateur évolue ici librement car on cherche juste la date où le matériel cesse de fonctionner (indépendamment du nombre de fois où le calcul est réalisé …)
Techniquement, TMR est disponible dès que state1+state2+state3>0. Cette interprétation signifie que l’architecture aura différents niveaux de fiabilité au cours de son utilisation. Dans ce cas précis, la disponibilité de TMR est plus grande que celle d’une réplique.
Question 3
Avec le nouveau critère de disponibilité (i.e. ce critère garantit la capacité de détecter une défaillance en valeur systématiquement), on voit la disponibilité de TMR chuter.