Le but de ce TP est de vous faire manipuler PRISM, un outil permettant la vérification de formules PCTL sur des chaînes de Markov. Nous allons d’abord faire la prise en main de l’outil.

Seule les réponses et modèles de la partie 3 sont à intégrer au rendu de TP noté pour cet énoncé de TP.

I Description du Système

Le diagramme ci-dessous représente la chaine que l’on souhaite que vous modélisiez pour une distribution initiale (0,1) (i.e. probabilité 1 d’être en 1). Cette chaine nous permet de modéliser la probabilité de l’activation d’une faute déclenchant une défaillance permanente à chaque exécution de notre système.

Figure 1 Représentation graphique de la chaîne modélisant une défaillance permanente.

On dira que 0 est l’état défaillant et 1 l’état fonctionnel.

A votre avis pourquoi ce diagramme de transition permet de retrouver la signification de chaque état simplement à partir de l’affirmation « A partir du moment où l’état du système devient défaillant, le système reste défaillant ».

Nous appellerons ce modèle permanentFail.

En vous inspirant du modèle permanentFail définissez (sur le papier) une chaine de Markov qui capture les informations suivantes (ce modèle sera appelé transientFail.

• Notre système démarre de manière certaine dans l’état fiable
• Traiter une requête entraine une transition vers les état ok, failed1 ou failed2 dont les valeurs sont respectivement 1,0,-1
• A partir de l’état ok le système lors du traitement d’une requête peut
  • soit rester dans l’état fiable avec probabilité 0.9,
  • soit défaillir de manière transitoire (failed2) avec probabilité 0.09,
  • soit défaillir de manière permanente (failed1) avec probabilité 0.01.
• Si le système tente de traiter une requête dans l’état défaillant, temporaire, le système l’aura détecté et appliquera un recouvrement avant ce qui garantit une exécution correcte et donc un retour certain dans l’état fonctionnel.
• Une défaillance permanente est …. permanente 🙂 et toute requête depuis cet état est défaillante et laisse le système en failed1.

Nous allons maintenant saisir ces modèles dans l’outil d’analyse PRISM.

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 depuis les machines de salle de TP, saisissez la ligne suivante :

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

Sinon téléchargez et installez l’outil depuis : https://www.prismmodelchecker.org/download.php
Compilez via make (rapide à priori)

Vous pouvez exécuter PRISM via la commande :

xprism

La fenêtre suivante s’affiche  :

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.

PRISM utilise une notation spéciale pour décrire des ensembles de transitions via une ligne (appelé command dans l’outil). Cette parie là est peut être la plus délicate. Consultez l’aide en ligne en cas de problème https://www.prismmodelchecker.org/manual/ThePRISMLanguage/Introduction

Détaillons la structure d’un modèle PRISM (pour plus de détail il vaudra mieux de toute manière aller consulter le manuel) :

• le type de modèle : dtmc (discret) ou ctmc (continu), mdp (markov decision process)… Cette information est fixée 1 fois par fichier
• 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. L’outil vérifiera lors de la génération du modèle que les contraintes de validité du formalisme sont respectée (i.e. somme probabilité sortante d’une chaine discrète =1 — ici param1 sera une probabilité). On notera par la suite que s et s’ désigne la valeur de l’état à la date courante et à l’instant d’après (pour décrire comment l’état se met à jour lors d’une transition).
• 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

La syntaxe de PCTL a été décrite en cours mais PRISM utilise des symboles spéciaux (‘[‘ et ‘]’) pour identifier les formules de chemin. Attention, vous devez de plus penser à bien mettre toutes les parenthèses dans vos formules. Vous le trouverez dans la section Property specification du manuel tout ce dont vous aurez besoin.

III Exercices

Exercice I

Recopiez le modèle fournit ci-dessous.

dtmc
module permanentFail
x : [0..1] init 1;
[] x=1 -> 0.9: (x’=1) +0.1: (x’=0);
[] x=0 -> 1: (x’=0);
endmodule

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 1.1 : Calculez la probabilité de réaliser 1, 2 puis 10 calculs successifs correctement pour le modèle permanentFail qui vous a été fourni ci-dessus.

Question 1.2 : On souhaite vérifier que la probabilité de rester dans l’état 1 indéfiniment est nulle. Trouvez la formule de chemin caractérisant cette contrainte puis utilisez l’opérateur P<=c (avec c une constante) pour vérifier l’affirmation ci-dessus.

Question 1.3 : On peut utiliser des Formules de chemin bornée dans le temps (ie. la contrainte instantanée ne doit être vérifier que sur des intervalles de temps bornés). Saisissez la formule suivante P>0.5 [G<=20 (x=1)] et vérifiez la.

Question 1.4 : En utilisant la syntaxe P=? et une formule de chemin, calculez la probabilité que le système soit toujours dans l’état 1 après 3 exécutions. (vous consulterez la syntaxe pour l’opérateur d’invariance G bornée)

Question 1.5 : Modifiez le modèle de sorte à rendre paramétrique le modèle et pouvoir indiquer la valeur de transition de l’état 1 à 0 en ne modifiant qu’une seule valeur (utilisez une constante).

Que se passe t il si la constante n’est pas initialisée lors d’une vérification ?

Nous allons voir comment utiliser ces paramètres pour explorer différentes hypothèses sur les probabilités.

Exercice 2

Question 2.1 : Définissez la formule permettant de verifier que le Système est dans l’état 1 pendant les 5 premières exécution du système avec probabilité 0.6. Trouver une valeur du paramètre rendant cette propriété vraie avec une précision de 0.1 (recherchez le à la main par tentatives successives).

Nous allons maintenant évaluer cette formule pour différentes valeurs associées au paramètre de manière automatique. Ceci est généralisable à N 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. ( si un seul paramètre l’outil le choisit pour vous )

Question 2.2 Réalisez l’expérience pour un intervalle [0, 1] avec un pas de 0.01. Le résultat est un tableau de booléen, trouvez la valeur maximale de votre paramètre à 0.01 près permettant de garantir la formule vraie.

Recommencez l’expérience en utilisant =? sur votre formule, et tracez l’évolution de la valeur

Question 2.3 : Modélisez le système transientFail (ci-dessus), paramétrez les probabilités de transition vers l’état transitoire et permanent avec un paramètre différent pour chaque

Question 2.4 Trouver la probabilité maximale que peuvent atteindre les deux types de défaillance associés au système de sorte que :

• la fiabilité du système reste supérieure strictement à 0.5 au bout de 5 exécutions. Le système est dit fiable à la date t, si il réussi 1 exécution correcte à partir de cette date.
• et que la défaillance transitoire soit 10 plus probable que la défaillance permanente.
• La valeur est trouvée à 0.001 près

Exercice 3

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éfaillante, une réplique ne peut redevenir fonctionnelle. Chaque réplique est indépendante des autres et défaille avec une probabilité de 0.005. 5.10e-3

Question 3.1 Définissez sous PRISM un module capturant le comportement d’une réplique, puis recopiez le deux fois en synchronisant les transitions des répliques.

Question 3.2 Le système est dit fiable à la date t, si il réussi 1 exécution correcte à partir de cette date. Fournissez la formule permettant de vérifier que la fiabilité du système est supérieur à 0.9 pour t=0, 10, 20,

Question 3.3 Comparez et commentez (est ce mieux strictement, moins bien … mieux sous conditions) la fiabilité d’une réplique à celle d’une réplication à 3 répliques pour t=1…300.

Question 3.4 Modifiez votre architecture pour passer à une réplication à 5 répliques et réévaluer la fiabilité d’une réplique vs l’architecture répliquée pour t de 1 à 3000 cette fois. Commentez le résultat.

Question 3.5 On souhaite pouvoir analyser une architecture active à 3 répliques dont les taux de défaillance sont respectivement 0.0005, 0.0005-lambda, 0.0005+mu.
a. Evaluer l’écart de fiabilité à t=10 pour les scénarios ou le couple (lambda, mu) vaut (0,0), (0.0004,0), (0,0.0005), (0.0004, 0.0004)
b. Comparez l’effet des ces couples sur l’intervalle de temps [10,300]. Commentez l’impact de ces variations de fiabilité dans une architecture à 3 répliques. Dans le cas (0.0004, 0.0004), peut on dire que les écarts de fiabilité se compensent ? Il vous est recommandé d’intégrer des tracés de courbes à votre rapport (via le mécanisme d’expérience).