I Description du Système

Nous considérons un système en charge de réaliser un asservissement (contrôle de système). Afin de garantir une bonne fiabilité et disponibilité des calculs, une architecture tolérante aux fautes est choisie: réplication active à trois répliques et un « voteur ». Nous disposons de données nous permettant d’affirmer que chaque calculateur subit des défaillances de type crash dont la date d’apparition suit une loi exponentielle de paramètre lambda de telle sorte que le temps moyen avant défaillance soit de 1000h. Nous considérerons que la minute est l’unité de temps utilisé dans les modèles. On suppose que les répliques sont totalement isolées. Ceci signifie que l’activation des fautes sur les différentes répliques sont des phénomène aléatoires indépendants.

II Lancement de l’outil de modélisation/analyse.

export PATH=/cal/homes/trobert/tool/prism-4.3.1-src/bin/:$PATH

xprism

La fenêtre suivante s’affiche  :

En cas de problème à utiliser la version pré-installée, vous avez toujours la possibilité de l’installer sur votre compte. Suivez ce lien (choisissez la version source code )

Dans la partie droite de cet écran, vous pouvez saisir votre modèle au format texte, c’est la vue Model (onglet en bas à gauche).

• le type de modèle : dtmc (discret) ou ctmc (continu) est fixé globalement
• les modules : le modèle est constitué de plusieurs modules chacun correspondant à une chaîne de Markov de même type. La déclaration d’un module commence toujours pas le mots clés « module » suivi d’un identifiant. Ensuite vient la déclaration de l’état, puis des transitions. La définition du module se termine par le  mot clés « endmodule« 
• Les transitions des modules peuvent être étiquetées afin de définir des transitions synchronisées au sens du produit classique d’automate: pour franchir une transition nommée « e » il faut que chaque automate franchisse une transition étiquetée « e ». Pour plus d’infos consulter la page sur les modules dans le manuel.
• Il est possible d’utiliser des constantes pour faciliter la modification des paramètres numériques d’un modèle. Ces constantes peuvent être initialisées dans le modèle, ou instancier à la volée lors des analyses. La syntaxe est « const <type> <identifiant> = <val> ;« . Les types supportés sont : int, bool, double.

Exercice 1

Recopiez le modèle suivant dans la fenêtre de modélisation:

dtmc
const double r=0.75;
module TMROnDemand
s: [0..3] init 3 ;
[] s>0 -> r : (s'=s) + 1-r:(s'=s-1);
endmodule

Ce modèle est proposé pour étudier la fiabilité de TMR pour le cas où l’on suppose que toutes les répliques sont actives et sans erreur au départ.

La ligne « [] s>0 -> r : (s’=s) + 1-r:(s’=s-1);  » décrit un ensemble de transitions en réalité.

Pour chaque valuation de s telle que s>0 (donc 1,2,3) il y a deux arcs sortants. Le « + » sépare les alternatives. Chaque arc est décrit par une probabilité « : » une règle de mise à jour où à l’instant k s’ correspond à \(s_{k+1}\) et s à \(s_k\). De manière pragmatique, s permet de compter le nombre de répliques fiables. Pour exploiter ce modèle, il est nécessaire de calculer une probabilité transitoire car la distribution de probabilité des valuations de s doit être évaluée pour un certain nombre d’arc franchis.  

Question 1 Il existe un instant pour lequel le calcul de la probabilité transitoire de chaque état permet de déterminer la probabilité des différents état fonctionnel et non fonctionnels d’une exécution de TMR. Déterminer ce nombre de transitions, puis calculer la probabilité que TMR fonctionne correctement à partir d’un état totalement fonctionnel en faisant évaluer la distribution transitoire de la chaîne à la date voulue.

Remarque : vous pouvez vérifier l’exactitude du calcul avec la formule suivante qui donne la fiabilité de TMR à partir du paramètre q représentant la fiabilité d’une réplique (en supposant que les états de fonctionnement des répliques sont des variables aléatoires indépendantes).

$$R(q)= q^3 +3 q^2(1-q)$$

Exercice 2

Un ingénieur prétend que le modèle ci dessus ne permet d’évaluer la fiabilité du système pour une séquence d’exécutions consécutives corrects. Nous allons essayer de comprendre pourquoi.

Réalisez les deux question suivantes sans utiliser PRISM

Question 1 évaluer la probabilité que TMR produise un résultat correct sachant qu’avant le début de l’exécution n répliques sont défaillantes (vous ferez le calcul pour n = 0…3)

Remarque pour n=0 et n=3 la réponse est triviale.

Question 2 Nous supposerons que la probabilité de défaillance d’une réplique fonctionnelle ne varie pas. Calculez la probabilité que TMR ait été fonctionnel pour deux traitements consécutifs sur l’architecture répliquée à partir de l’état où toutes les répliques sont fonctionnelles (utilisez les valeurs précédemment demandées)

Remarque : cela revient à calculer la probabilité que TMR fonctionne correctement une fois (utilisez la formule précédemment fournie), et qu’en fonction de l’état fonctionnel (2 répliques correctes ou 3 répliques correctes) TMR puisse rester dans un état fonctionnel encore une fois.

En résumé, vous devriez constater que le premier modèle est pessimiste d’environ 10% (on passe ~60% à 54% de fiabilité).

Nous allons essayer de retrouver ce résultat via PRISM puis le généraliser.

Il est possible de représenter un réseau de chaines de Markov sous PRISM. Cependant, il faut bien comprendre le lien entre un tel modèle à temps discret et l’écoulement du temps.

Pour comprendre ce lien, nous prendrons le cas très simpliste de chaines de Markov déterministes nommées C1, C2: pour i=1,2 leur état « Si » est inclus dans 0..5, et initialisé à 0 de plus

\(P(Si(k+1)=(Si(k)+1) mod 6|Si(k))=1\), ou mod et l’opérateur modulo (attention dans le code la notation change légèrement).

Voici comment une telle paire de chaînes peu être définie :

dtmc 
module C1
S1 :[0..5] init 0;
[] true -> 1: (S1'=mod(S1+1,6));
endmodule

module C2 = C1[S1=S2] endmodule

Analysons la déclaration : la déclaration de la première chaine est très standard. La seconde chaîne est déclarée par duplication. Le principe est de donner le nom du modèle à copier (ici C1 puis de détailler les substitution de noms de variables à réaliser). Admettons que l’on ait une chaîne nommée old, dont l’état est oldS. On peut créer la chaîne new d’état newS comme ceci module new = old[oldS=newS] endmodule. Pour plus de détails consultez le manuel. Évaluez la formule P=? [F[1,1] (S1=1 & S2=1)]

Remarque : il y  a une hypothèse implicite lors de cette analyse. Lorsque plusieurs chaînes peuvent progresser, il y a un tirage de loi uniforme pour savoir laquelle progresse. Comme les transitions ne sont pas synchrone, une seule est franchie à chaque incrément du temps. Il est possible de nommer les transitions ce qui permet de les synchroniser.

Modifier le modèle en ajoutant un identifiant quelconque entre les deux crochets au début de la ligne décrivant les transitions de C1. Évaluez la formule P=? [F[1,1] (S1=1 & S2=1)]

Question 4 Proposez un modèle composé de trois chaînes de markov, une pour chaque réplique. Sous l’hypothèse que les états de ces répliques sont x1,x2,x3, alors l’état de fiabilité de TMR doit pouvoir s’exprimer comme \(x1+x2+x3\ge 2\)

Vérifiez que vous obtenez bien les mêmes valeurs de fiabilité que dans l’exercice 1.

Question 5 Définissez la formule PCTL permettant d’évaluer la probabilité que l’architecture reste fiable durant dix sollicitations consécutives à partir de son état initial.

Il est possible d’utiliser des constantes que vous pourrez faire varier lors d’une expérience pour évaluer des variantes d’une formule. Pour cela, vous devez ajouter la dite constante dans la fenêtre Properties avant de l’utiliser dans la partie formule. De plus il est possible de faire varier plus d’une constante à la fois lors d’une expérience, il convient tout de même de dire celle qui servira de base pour l’axe x. Les autres variantes correspondront à différentes courbes.

Question 6  Utilisez une constantes pour évaluer la variation de la fiabilité de TMR pour un nombre T d’exécutions consécutives variant de 1 à 20 (prenez un pas de 1), et une autre constantes pour évaluer l’impact de la probabilité de défaillance d’une réplique sur ces courbes pour l’intervalle [0.75 1] avec un pas de 0.05.

Vous devriez obtenir quelque chose comme cela :

Anecdote :  sur un avion on peut arriver à exiger plusieurs heures de fonctionnement sans aucune défaillances. Pour des applications s’exécutant toutes les 10 ou 100 ms, je vous laisse imaginer ce qu’il faut comme fiabilité de base pour les dits composants. (on utilise des choses plus avancé qu’un simple TMR d’un autre coté).

Exercice 3

Dans ce dernier exercice, nous nous intéressons à la modélisation de la disponibilité du système.  Nous distinguons fiabilité et disponibilité en supposant que le logiciel subit des défaillances en valeur tandis que le matériel est sujet aux défaillances silencieuses (aussi appelées crashs). Ainsi, il faut décider que quels sont les états de disponibilité du système. En effet, si un calculateur crash, le fonctionnement logique de TMR est affecté car le vote doit se faire sur 2 répliques. Dans le cas extrême, on peut considérer l’architecture disponible mais peu fiable si l’on accepte que tant qu’un calculateur est en service, alors la fonction délivrée par TMR est disponible.

En supposant que n désigne le nombre de réplique non « crashées », dans ce tp TMR est déclarée disponible tant que \(n\ge 1\).

Question 1 Modéliser le comportement d’un calculateur dont la date de défaillance suit une loi exponentielle dont le paramètre est appelé taux de défaillance.  Modéliser un calculateur dont le temps moyen avant défaillance est de 100h. Définissez le modèle pour que la minute soit l’unité de temps. (utilisez une constante comme dans le premier cas).

Notez : pour les chaines continues, on ne définit pas les « self-transitions » i.e. les boucles. De plus la somme des taux est libre (elle n’a pas d’obligation à faire 1. La moyenne d’une loi exponentielle est l’inverse de son taux).

Il est possible de sauvegarder les données d’une expérience PRISM sous différents formats. Si vous exportez les données d’une expérience ou vous faite variez une constante représentant le temps (e.g. T). Il devient possible de calculer le temps moyen pour qu’une certaine transition soit prise.

Question 2 Utilisez une expérience permettant d’avoir, pour chaque instant jusqu’à 10000, la probabilité d’être dans l’état défaillant. Pour cela, vous pourrez engendrer la courbe correspondant à P=?[F[T,T] Q] avec Q la formule indiquant l’état de défaillant de votre réplique. Puis, utilisez un tableur ou le script R fourni ci-dessous pour calculer la date moyenne de la transition de l’état fonctionnel vers celui de défaillance.

#!/usr/bin/Rscript
args<-commandArgs(TRUE)
table <- read.csv(file=args[1], head=FALSE,skip=1,sep=",")
u<-table$V1
v<-table$V2
r<-diff(v)*u[-1]
print(sum(r))

ATTENTION : le produit synchronisé de chaines n’a pas beaucoup de sens pour les chaines continues (car PRISM multiplie les taux associés aux transitions). Il faut donc laisser les transitions non synchronisées.

Question 2 Définissez un produit de chaînes continues permettant de modéliser la disponibilité de TMR et son temps moyen de passage en état indisponible.

Question 3 Refaites le calculs pour un critère  de disponibilité exigent qu’au moins deux répliques soient disponibles (afin de pouvoir détecter une erreur de calcul).

A- t-on gagné en disponibilité avec TMR ?