Nous nous intéressons aux erreurs qui apparaissent lors de la vérification de systèmes probabilistes en utilisant la technique d’évaluation de modèle avec l’outil PRISM. L’évaluation de modèle probabiliste est une technique de vérification qui consiste à déterminer si un modèle probabiliste M vérifie une propriété donnée. Les modèles sont décrits par des systèmes de transitions tandis que la logique temporelle est utilisée comme langage de spécification des propriétés. L’algorithme d’évaluation de modèle qui est appliqué consiste essentiellement à résoudre un système d’équations linéaires Ax = b. Nous montrons à quelles étapes du processus d’évaluation de modèle les erreurs apparaissent. Nous distinguons essentiellement deux types d’erreurs à savoir les erreurs d’arrondi (arithmétique à point flottant, model-checking symbolique), et les erreurs de troncature qui proviennent du fait qu’on a remplacé une méthode de calcul direct par des opérations mettant en jeu un nombre fini d’étapes. Nous utilisons la notion de bisimulation approchée pour comparer le modèle M à l’étude et celui réellement encodé par PRISM. Nous faisons aussi une analyse numérique de l’écart entre la solution x du système linéaire Ax = b et celle calculée par PRISM suite aux effets de l’erreur d’arrondi. / We are interested in errors that occur during the verification of probabilistic systems using the technique of model-checking with PRISM tool. Probabilistic model-checking is a technique for verification that aims at determining whether a probabilistic model satisfies a given property. The models are described by transition systems while temporal logic is used as specification language for properties. The model-checking algorithm under study essentially involves solving a system of linear equations Ax = b.We show at what stages of the model-checking process the errors appear. We basically distinguish two types of errors, namely rounding errors (floatingpoint arithmetic, symbolic model checking), and truncation errors, which arise because a direct method of calculation is replaced by operations involving a finite number of steps. We use a notion of approximate bisimulation to compare the model under study and the one actually encoded by PRISM. We also carry a numerical analysis of the difference between the solution of the linear system Ax = b and the one calculated by PRISM, due to the effects of rounding errors.
| Identifer | oai:union.ndltd.org:LAVAL/oai:corpus.ulaval.ca:20.500.11794/25469 |
| Date | January 2014 |
| Creators | Muhimpundu, Joël |
| Contributors | Desharnais, Josée, Laviolette, François |
| Publisher | Université Laval |
| Source Sets | Université Laval |
| Language | French |
| Detected Language | French |
| Type | info:eu-repo/semantics/masterThesis |
| Format | 1 ressource en ligne (xv, 106 pages), application/pdf |
| Rights | info:eu-repo/semantics/openAccess, https://corpus.ulaval.ca/jspui/conditions.jsp |
Page generated in 0.0081 seconds