I Description du Système

Nous allons modéliser la fiabilité d’une fonction de calcul qui réalise un calcul de manière périodique. La fonction de calcul possède une probabilité de subir l’activation d’une faute de développement : \(dev_F=0.1\).  On supposera que la conséquence de l’activation est l’arrêt du calcul et que toute nouvelle tentative de calcul se soldera par la même défaillance. Nous allons modéliser ce comportement par une Chaîne de Markov.

Rappel : une chaîne de Markov discrète correspond à définir une séquence de variables aléatoires \( X_0, X_1,…X_{n,n\in \mathbb{N}}\), telle que \(P(X_j=v_j | X_i=v_i,\forall i<j)= P(X_j=v_j|X_{j-1}=v_{j-1})\).

Cette connaissance peut être modélisée en représentant les probabilité de « change \(v_j-1\) en \(v_j\)

Ainsi, pour modéliser une chaîne correspondant à une séquence de variable X telle que :

• la probabilité que X soit différent de 0 ou 1 est nulle,
• si \(X_k\) vaut 1 alors \(X_{k+1}\) vaut 1 avec probabilité 0.9, et 0 avec une probabilité 0.1.
• si \(X_k\) vaut 0 alors \(X_{k+1}\) vaut 0 avec probabilité 1. (pas de retour à 1)

Le diagramme ci-dessous représente cette chaîne :

Figure 1 Représentation graphique de la chaîne modélisant un « crash ».

Chaque arc est appelé une transition. Supposons que cette chaîne représente l’état d’une fonction devant être exécutée périodiquement mais pouvant subir une défaillance de type crash à chaque exécution (supposons le crash  permanent). Une transition représente l’écoulement d’une période (durant laquelle un calcul doit avoir lieu).

Question 1 : quelle valeur représente l’état « crashé » de la fonction ?

Nous souhaitons raffiner notre modèle. Pour chaque période (i.e exécution du calcul), soit le calcul déclenche l’arrêt (crash) de la fonction avec probabilité 0.1, soit il déclenche la production d’une valeur incorrecte avec une probabilité 0.15 (nommé \(int_F\)). Dans les deux cas la défaillance est permanente. Cependant, une fois dans l’état correspondant au cas défaillance en valeur, le système a aussi la possibilité d’activer la faute menant à l’arrêt du calcul (probabilité 0.1).

Question 2 : Modifiez le modèle donné ci dessus pour représenter ce changement de modélisation (sur papier)

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

export PATH=/cal/homes/trobert/tool/prism-4.3-linux64/bin/:$PATH

xprism

La fenêtre suivante s’affiche  :

Au cas où vous ne pourriez utiliser la version pré-installée en salle de tp à Télécom, vous avez toujours la possibilité de l’installer sur votre machine. Suivez ce lien (choisissez la version qui vous convient.

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

Voici le texte correspondant à la chaîne décrite en figure 1.

1. dtmc
2. module myfunction
3. x : [0..1] init 1;
4. [] x=1 -> 0.9: (x’=1) +0.1: (x’=0);
5. [] x=0 -> 1: (x’=0);
6. endmodule

Détaillons les lignes ci dessus rapidement. Lors de la définition d’un modèle PRISM vous devez préciser :

• le type de modèle : dtmc (discret) ou ctmc (continu). Cette information est fixée globalement
• les descriptions de modules : le modèle peut être constitué de plusieurs modules. Vous considérerez dans un premier temps qu’un seul module est défini et qu’il correspond à la chaîne étudiée via PRISM.
• La déclaration d’un module commence toujours pas le mots clés « module » suivi d’un identifiant. Ensuite vient la déclaration de la/les variable(s)  d’état, puis des transitions. La définition du module se termine par le  mot clés « endmodule« 
• La déclaration de la variable se fait comme suit : « s : [3..6] init 4; » pour une variable nommée s dont la valeur est forcément dans [3,6] et est initialisée à 4 à l’instant initial.
• Les transitions entre états sont toujours structurée de la même manière :
  « [] <garde> -> <param1> :(<maj1>)+<param2> :(<maj2>); ». Cf la ligne 3 dans le modèle ci-dessus. Pour plus d’infos consulter la page sur les modules dans le manuel. Attention la garde peut représenter plusieurs états.
• Il est possible d’utiliser des constantes pour faciliter la modification des paramètres numériques d’un modèle. La syntaxe est « const <type> <identifiant> = <val> ;« . Les types supportés sont : int, bool, double. Ces lignes doivent être insérées juste en dessous du type de modèle
  

III Exercices

Exercice I

Recopiez le modèle fournit ci-dessus. Cliquez droit dans la fenêtre modèle et sélectionnez « Compute -> Transient Probability ». On vous demande de saisir un nombre qui correspond au nombre de transition franchie (i.e. à l’indice k pour lequel on cherche la distribution de probabilité de \(.

Question 3 : Calculez la probabilité de réaliser 1, 2 puis 10 calculs successifs.
indice : Dans l’affichage textuel recherchez la ligne « Printing transient probabilities in plain text format below: »

L’onglet Properties (à sélectionner en bas) fait apparaître une nouvelle vue. Il est possible d’y saisir des formules dite PCTL (cf cours). Ces formules permettent de sélectionner un ensemble de séquences de valeurs [latex] x_0….x_k \) telles que ces séquences de valuations de la variable x satisfassent une formule LTL. La documentation est ici 

Sur cet ensemble, différentes opérations sont réalisables :

• vérifier une contrainte sur la probabilité qu’une réalisation de \( X_0, X_1,…X_{n,n\in \mathbb{N}}\) corresponde à l’un de ces chemins. (En utilisant P<contrainte> [<formule LTL>]
• Demander à calculer la probabilité qu’une formule LTL soit vraie
  P=? [<formule LTL>]

Par exemple, la propriété [/latex]F (x=0)[/latex] correspond à l’ensemble des chemins où l’on finit par avoir \(X_k=0\). Ainsi, P>=1[F (x=0) ] sera soit vraie, soit fausse sur notre modèle. (dans notre cas ce sera vrai)

Mise en pratique  : cliquez droit dans la partie en haut à gauche de l’interface et faites « Add ». Copiez collez ce texte : P=? [ F(x=0)]. Puis faites clique droit pour et sélectionnez « Verify ». Vous devriez voir que l’outil vous indique que cette propriété est vraie (probabilité de 1).

Il est possible de restreindre les chemins sélectionnés par une formule en ajoutant des contraintes numériques sur les dates de changement d’état (ici on peut contrôler la date à la quelle la formule Q doit être vrai dans (P U Q). Cela se fait en ajoutant juste après l’opérateur U soit un intervalle de date, soit une contrainte du type « <=c » ou « >c » où c est une valeur entière.

Question 4 : Introduisez une contrainte à la formule précédente pour calculer la probabilité que x reste à 1 pendant au moins 2 périodes à partir de l’état initial (i.e. vous devriez retrouver la valeur 0.81).

Question 5 : Modifiez le modèle pour y définir la probabilité de rester dans l’état 1 via un paramètre (on vous demande de faire en sorte que l’intégralité du modèle soit cohérente si la valeur du paramètre venait à changer).

Enregistré le modèle courant (par exemple sous le nom singlefault.prism ) , puis faites enregistrer sous pour sauvegarder une copie sous le nom twofault.prism par exemple.

Question 6 : Modifiez le modèle pour y intégrer le second type de faute décrit en question 2 et faire en sorte que les deux probabilités d’activation des fautes puissent être modifiées (utilisez un paramètre.

indication : attention pour chaque ligne de transition commençant par une garde, vous devez décrire toutes les transitions sortant de cet ensemble d’état. Par exemple, pour l’état 1, nous avons décrit par une seule ligne (ligne 4), 2 transitions. Sur chaque ligne la somme de probabilité doit faire 1 pour un modèle discret.

Exercice II Exploration d’un espace de modélisation

Il a déjà été dit que la vision probabiliste ne faisait pas forcément l’unanimité. Une raison réside dans le fait qu’il n’y a pas forcément pour un même système de consensus sur la définition des distribution de probabilité le caractérisant.

Pour pallier ce problème, il est possible de paramétrer les modèles, et les propriétés pour répondre à différentes questions.

Vous avez déjà paramétré votre modèle pour le cas 2 fautes.

Question 7 : Modifiez ce modèle de sorte à supprimer l’initialisation (pas la déclaration ) de ces constantes. Vérifiez la formule P=? [G<=10 (x=1)] en l’ajoutant dans la section Properties. Vérifiez cette formule (click droit …) pour une valeur de paramètre de 0.05 et 0.1 (pour le respectivement les défaillances en valeur et crash).

NB: la valeur 1 pour x représente l’état fonctionnel a priori (adaptez en fonction).

Nous allons maintenant évaluer cette formule pour différentes combinaisons de valeurs associées aux paramètres. Dans la section « Properties », cliquez droit dans la fenêtre d’édition du modèle et sélectionnez « new experiment ». Cela va ouvrir une fenêtre qui propose soit d’affecter les constantes soit de les faire varier dans un intervalle définit par « start » et « end ». Le principe est que différentes valeurs du paramètre seront choisies puis la vérification se fera avec cette affectation des paramètre du modèle. Une fois le chois du domaine de variation réalisé vous devez choisir quel paramètre sera utilisé pour l’abscisse. Les autres paramètres serviront à tracer différentes courbes identifiables par leur noms.

Question 8 : Réalisez une expérimentation pour visualiser comment évolue la probabilité d’une exécution fiable sur 10 itérations consécutives de la fonction en fonction des deux paramètre \(dev_F,\; int_F\) (respectivement crash et défaillance en valeur).

Question 9 : Trouver la probabilité maximale que peuvent atteindre les deux types d’activation de fautes associées au système de sorte que :

• la fiabilité du système reste supérieure ou égale à 0.5,
• et que les deux phénomène aient la même probabilité d’occurrence.
• On acceptera une erreur inférieur à 0.001 à la fiabilité qui découle de la valeur que vous proposerez

Question additionnelle : on veut maintenant évaluer la disponibilité du système. Dans le cas d’une défaillance non permanente, il est difficile de l’évaluer avec des formules PCTL (voir impossible). Il en découle que l’on peut utiliser une structure de récompense pour évaluer cette propriété.

Vous utiliserez les valeurs de paramètres trouvé à la question précédente.

Question 10 : Introduisez un système de récompense simple sur l’état 1 pour évaluer la disponibilité du système. cf manuel ici pour la définition.

Consultez la page de manuel ici pour l’évaluation de la récompense. 

Question 11 : Introduisez un système de récompense pour évaluer le nombre de défaillance, et le temps passé dans l’état défaillant transitoire. 

III Modélisation d’une stratégie de réplication

On suppose que l’on souhaite étudier la fiabilité d’un système reposant sur la réplication active à 3 répliques avec seulement un mode de défaillance (byzantin). Dans ce cas, si plus d’une défaillance a lieu, on suppose que toutes les répliques produisent la même valeur fausse…

Une fois défaillant, une réplique ne peut redevenir fonctionnelle. Chaque réplique est indépendante des autres et défaille avec une probabilité de 0.25. On suppose que le voteur est cependant sans mémoire (il ne tient pas compte des défaillances précédentes).

Question 10 Définissez sous PRISM une chaîne de Markov qui capture le nombre de réplique défaillantes à chaque instant (une transition modélisant l’exécution de l’architecture complète), On suppose toute les répliques fonctionnelles initialement et indépendantes (avec même probabilité de défaillir). Calculez la probabilité de produire un résultat correcte à la date 1.

Question 11 Réalisez une expérience pour trouver la probabilité de défaillance (approximation à 0.01 près) qui garantit une fiabilité de 0.99 au bout de 10 itérations.