Pages professionnelle – Thomas Robert

Maître de Conférence

Vérification de chaine de Markov II

Le but ici est de vous faire expérimenter certaines subtilité de l’outil PRISM. Ce TP se terminera par un problème de modélisation « ouvert ». Dans ce cas, nous vous encourageons à discuter entre vous pour déterminer comment le modéliser.

Nous allons partir du modèle ci dessous qui est définit à partir d’un produit de chaines de Markov:

dtmc 
const double rel;// rel = reliability
module rep1 
x1:[0..1] init 1 ; 
[] (x1=1)->rel: (x1'=x1)+ (1-rel):(x1'=0);
[] (x1=0)->1: (x1'=x1);
endmodule
module rep2=rep1[x1=x2] endmodule 
module rep3=rep1[x1=x3] endmodule 

La propriétés intéressante pour ce modèle est :

// probabilité de n'avoir jamais défailli jusque'à la date T
P=? [G<=T (x1+x2+x3>=2)]

Tracer cette probabilité pour T partant de 1 à 20, pourquoi ce résultat est différent du résultat que vous pourriez obtenir en analysant le modèle suivant réponse à la dernière partie du TP 1 :

dtmc
const double rel;
module triple
//frep stands for functional replica
frep : [0..3] init 3; 
[] (frep=3)-> rel*rel*rel :(frep'=frep)+ 3*rel*rel*(1-rel):(frep'=2)
		+ 3*rel*(1-rel)*(1-rel):(frep'=1)+(1-rel)*(1-rel)*(1-rel):(frep'=0);
[] (frep=2)-> rel*rel :(frep'=frep)+ 2*rel*(1-rel):(frep'=1) +(1-rel)*(1-rel):(frep'=0);
[] (frep=1)-> rel:(frep'=frep)+ (1-rel):(frep'=0);
[] (frep=0)-> 1:(frep'=0);

endmodule

Un ingénieur propose de tracer P=? [F[3*T,3*T] (x1+x2+x3>=2)] est ce que cela changerait quelque chose ? A quoi est dû le problème ?

Modifiez le modèle de sorte que P=? [F[T,T] (x1+x2+x3>=2)] capture la fiabilité du système au bout de T exécutions.

Nous souhaitons modéliser le fait qu’une réplique peut défaillir mais que cette défaillance peut à chaque nouvelle exécution être détectée et l’état du système réinitialisé à correct pour l’exécution suivante.

Proposez une modification du modèle capturant ce phénomène en partant de l’hypothèse que cette détection recouvrement a lieu avec probabilité detect sachant que le système a défailli (en gros il va falloir revoir peut être les transitions ou les états ). On souhaite maintenir le fait que P=? [F[T,T] (x1+x2+x3>=2)] capture la fiabilité du système au bout de T exécutions.

Comparer la fiabilité de ce système pour une probabilité de détection de 0,5 à chaque état avec la fiabilité du système sans détection mais avec une probabilité de défaillance divisée par 2. (on suppose toujours la probabilité de défaillance égale au départ à 0.75