Analyse quantitative de fiabilité / disponibilité

Nous souhaitons calculer 2 valeurs clés de la fiabilité / disponibilité d’un système pour une réplication active à 3 répliques :

• La probabilité instantanée de produire un résultat correcte
• La probabilité de réaliser moins de 5 exécutions incorrectes consécutives lors des 100 premières exécutions du système.

Nous supposerons un modèle de réplique qui a un seul mode de défaillance (byzantin) et qui possède un mécanisme de réparation « instantané » pour une réplique qui défaille. Cependant, cette réparation n’a lieu qu’avec une probabilité de 0.2. La défaillance byzantine du système a elle pour probabilité d’occurrence 0.05.

Proposez un modèle permettant de capturer cette probabilité ?

Indices : parfois la vérification d’une formule nécessite de synchroniser un autre module qui construit pas à pas un état complexe à partir duquel la formule s’exprime du coup simplement.

On souhaite désormais utiliser le mécanisme de récompense pour évaluer le nombre moyen d’exécutions correctes sur 100 exécutions.

Utilisez une structure de récompense sur les états et une propriété de récompense de type requête de calcul cumulatif (cf manuel PRISM).

On suppose désormais que la probabilité de défaillance d’une réplique est un paramètre : failure. On souhaite déterminer si pour une probabilité de défaillance arbitraire entre 0.001 et 0.2, il est possible de trouver un facteur multiplicatif r minimal tel que si recover=r*failure, alors la probabilité de produire 5 résultats faux consécutifs est inférieure à 0.0001.

Est ce possible ? Trouvez la valeur de r.