Pages professionnelle – Thomas Robert

Maître de Conférence

TP analyse quantitative I

Le but de ce TP est de vous faire manipuler PRISM, un outil permettant la caractérisation des attributs de sûreté de fonctionnement : fiabilité et disponibilité.
Le TP est découpé en trois parties, mais tout d’abord nous allons décrire le système étudié.

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.

L’outil PRISM permet de spécifier des chaînes de Markov et autres processus stochastiques, puis de réaliser des analyses sur ces derniers. Concernant les chaînes de Markov, les analyses suivantes sont possibles :  calcul de la probabilité stationnaire pour déterminer vers quelle distribution d’état « converge » la chaîne, ou un calcul sur un état transitoire pris à une date précise. Il est possible de généraliser le dernier cas en évaluant la probabilité qu’une formule de type PCTL soit vraie pour une chaîne donnée.
Pour lancer l’outil, saisissez la ligne suivante :
export PATH=/cal/homes/trobert/tool/prism-4.3-linux64/bin/:$PATH
Une fois cette ligne saisie, vous pouvez exécuter PRISM via la commande :

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 source code ) et compilez la via make. Cela devrait être très rapide.

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. 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=? [(x=1) U (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.

Voici le résultat que vous pourriez obtenir pour le premier modèle (singlefault.prism) si l’on faisait varier la probabilité d’éviter le crash de 0 à 1  (lors de la vérification de P=? [G<100!(x=0)]
(nous ne prenons pas le modèle à traiter dans l’exercice pour que vous ayez différents exemples ).

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

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.

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. 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.