Pages professionnelle – Thomas Robert

Maître de Conférence

TP Vérification de Chaînes de Markov I – PRISM

Le but de ce TP est de vous faire manipuler PRISM, un outil permettant la vérification de PCTL sur des chaînes de Markov (et de nombreux autres modèles). Nous allons d’abord faire la prise en main de l’outil. Puis vous devrez l’utiliser pour retrouver des résultats classiques concernant la disponibilité et la fiabilité de la réplication active.

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

Vérifiez votre compréhension du sens pratique des états 1 et 0

  • Quel état représente la défaillance permanente,
  • Quel état représente un fonctionnement correct.

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
  • le système ne peut changer d’état que si il traite une requête.
  • A partir de l’état fiable 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 avec probabilité 0.09, soit défaillir de manière permanente.
  • 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 :).

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.

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

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 parami sera une probabilité).
  • 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 de parenthésage spéciaux (‘[‘ et ‘]’) pour identifier les formules de chemin.

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 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 : Allez dans l’onglet property et saisissez la propriété qui est vraie ssi la probabilité de rester dans l’état fonctionnel au bout de 5 exécutions est supérieur à 0.5.

Question 1.3 : Ajouter la propriété permettant de vérifier qu’il est quasi certain que l’on finisse dans l’état défaillant

Question 1.4 : Quelle est la formule permettant de vérifier qu’il est vraisemblablement certain (i.e. probabilité 1) que ce système une fois défaillant ne peut pas se réparer.

Les solutions à ces premières questions seront fournies dans le chat du cours au fur et à mesure.

Question 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 ?

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

Exercice 2

Question 2.1 : Modifiez le modèle permanentFail de sorte que la probabilité de défaillance soit définie par un paramètre.

Question 2.2 : Vérifiez que la probabilité de la formule de chemin exigeant que la cinquième exécution de votre système est correcte soit strictement supérieure à 0.5 pour une valeur de paramètre de comprise entre 0 et 1.

Nous allons maintenant évaluer cette formule pour différentes valeurs associées au paramètre. 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.3 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.

Au lieu d’une contrainte sur l’opérateur logique P on peut utiliser l’expression ‘=?’ pour demander le calcul de la probabilité de [[Formule]] (pour la propriété P=?[Formule]).

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

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

Question 2.5 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,
  • et que la défaillance transitoire soit 10 plus probable que la défaillance permanente.
  • La valeur est trouvée à 0.001 près

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 un unique module capturant par transition l’intégralité du changement d’état de la stratégie de réplication

Indication : un module avoir plusieurs variables d’état déclarée.

Question 11 Quelle est la fiabilité de cette architecture au bout de 20 itérations comparée à la fiabilité d’une seule réplique ?