Chap 7 1 Chapitre 4 Vérification de modèles: Automates de Büchi et SPIN (Holzma
Chap 7 1 Chapitre 4 Vérification de modèles: Automates de Büchi et SPIN (Holzmann Chap. 6) http://w3.uqo.ca/luigi/INF6001/ INF6001 Chap 7 2 Propriétés d’états et exécutions (chaînes) X=13 X=X/2+1 X>0 X=X/2 X≤0 s0 Nous pouvons affirmer des propriétés pour: Des états: p.ex. à l‟état s1, X=13 toujours (invariant) pas besoin de logique temporelle ici Des exécutions, p.ex. x≤0 ou x≤0, mais pas x≤0. Observez que dans ce cas le contrôle est sur les transitions. s1 s2 s3 X: entier et / a résultat entier . État d‟acceptation INF6001 Chap 7 3 Comment vérifier les propriétés temporelles? Nous avons une machine dont nous pouvons observer certaines propriétés, p.ex. qu‟une variable a toujours une certaine valeur ou une propriété temporelle Solution: exécuter la machine en parallèle avec une autre machine qui observe et vérifie ces propriétés – composition synchrone nous pouvons aussi vérifier une propriété négative, c.-à.-d. que la machine ne satisfait pas une propriété never automata INF6001 Chap 7 4 Vérification de modèle Modèle à vérifier Machine exprimant des propriétés à vérifier Composition synchrone INF6001 Chap 7 5 Exemple s 1 p AB pour vérifier p Cet AB synchronise avec un autre AB seulement si la propriété p reste toujours vraie, à toutes les transitions 6 Acceptation dans les automates de Büchi Un automate régulier accepte toutes les chaînes qui conduisent à un état final Un AB accepte toutes les chaînes infinies qui passent un nombre infini de fois par un état final Pour chaque expression de logique temporelle, il y a un AB qui accepte les chaînes qui satisfont cette expression Il existe un algorithme pour effectuer cette construction, pas discuté dans ce cours INF6001 Chap 7 7 Incomplétude des AB L‟AB de gauche ne considère pas le cas de recevoir un p Ceci simplifie la compréhension et la vérification, car les transitions qui ne conduisent pas au résultat désiré ne sont pas prises en considération s 1 p s 1 p s 2 p INF6001 Chap 7 8 Exemple s 0 s 1 p p true AB pour vérifierp Cet AB est prêt à accepter des transitions où p est faux, mais il est content seulement quand p devient vrai. INF6001 Chap 7 10 Exemple AB pour vérifier que p (enfin toujours p) „true‟ accepte p et autres mais après un certain p, il n‟accepte que des p après s 0 s 1 true p p INF6001 Chap 7 11 Comparer avec AB déterministe s 0 s 1 ¬p p p L‟AB ci-dessous n‟est pas bon pour p Car s‟il y a un 1er p qui n‟est pas suivi par p il rejette. Il faut dans ce cas continuer à chercher un p futur après lequel p Cet AB montre aussi les limites de l‟expressivité des opérateurs , car ce qu‟il exprime (après le 1er p, toujours p) n‟est pas exprimable avec ces opérateurs seulement. faut utiliser U: ¬ p U p INF6001 Chap 7 16 Autre exemple impliquant U (until fort) s 0 s 1 p q true p U q INF6001 Chap 7 18 Exemple s 0 s 1 true p p toujours finalement p (infiniment souvent p) true Accepte seulement quand il continuera d‟y avoir des p dans le futur INF6001 Chap 7 20 Exemple: utiliser les notions d’équivalence p = p Un p doit être trouvé, après on peut trouver autre chose, mais il faut retourner sur p s 0 s 1 true true p toujours finalement p INF6001 Chap 7 21 Exemple (pas très intuitif, mais…) (p q) = ( p q) Dorénavant, un p est suivi toujours par un q. Utilisant la formule de droite, nous voyons que: à cause du fait que faux vrai = vrai, p n‟a pas besoin de se produire afin que q se produise et rende la formule vraie INF6001 Chap 7 22 Exemple continuation (p q) = ( p q) s 0 s 1 p q true q true Accepte tant que p q est vrai, peut aussi passer à un état où un q doit se produire plus tard Dorénavant, un p est suivi toujours par un q INF6001 Chap 7 24 Never claims: exigences négatives Nous verrons qu‟en principe il est plus efficace de contrôler l‟absence de comportements défendus plutôt que de contrôler que tous les comportements soient permis L‟AB approprié est donc obtenu par négation d‟une formule de logique temporelle INF6001 Chap 7 25 Négation de la formule précédente: (p q) = ( p q) Dorénavant, un p est suivi toujours par un q Donc cette formule est fausse s‟il y aura un p et puis aucun q INF6001 Chap 7 26 Automate négation: never automata Supposons que nous voulions qu‟un comportement niant la formule précédente soit détecté: (p q) = par définition de ( p q) = par loi de dualité ( p q) = par loi de De Morgan (p q) = par dualité (p q) s 0 s 1 true p q q Donc si un comportement tombe dans l‟état s1, il n‟est pas conforme aux exigences INF6001 Chap 7 27 Propriétés d’un système Pour prouver qu‟ un système jouit des propriétés spécifiées par des expression de logique temporelle, il faut montrer que tous les comportements du système ont ces propriétés Nous appelons „langage‟ d‟un automate l‟ensemble de chaînes, l‟ensemble des comportements, qu‟il accepte Propriétés ou exigences positives Toutes les exécutions du système satisfont aux propriétés Pour prouver une exigence positive, nous devons prouver que le langage du système est inclus dans le langage de l‟AB qui exprime l‟exigence Propriétés ou exigences négatives Aucune exécution du système ne satisfait aux propriétés Le langage du système et le langage de l‟exigence doivent avoir intersection vide Si l‟intersection est non vide, les exécutions dans l‟intersection sont des contre- exemples, montrant dans quelles situations la propriété est violée Deux manières de prouver ou refuser une propriété Prouver que tous les comportements du système satisfont la propriété Chercher un comportement du système qui satisfait la négation de la propriété! (un contrexemple) Clairement, cette deuxième stratégie pourrait aboutir plus rapidement, car dès qu‟un contrexemple est trouvé, nous savons que la propriété est fausse et nous n‟avons pas besoin de continuer INF6001 Chap 7 28 Never claims Donc un model checker comme SPIN systématiquement nie les propriétés qu‟on veut vérifier et cherche un contrexemple au lieu de chercher à prouver que une propriété souhaitée est toujours vraie Si un contrexemple est trouvé, on sait que la propriété est fausse et on a sauvé du temps Si un contrexemple n‟est pas trouvé, on sait que la propriété est vraie et on a fait le même travail que dans le cas où on aurait cherché à prouver la propriété positive directement Les propriétés niées s‟appellent never claims INF6001 Chap 7 29 INF6001 Chap 7 35 Preuve d’exigences négatives Étant donné un système S et une formule LTL f à contrôler pour S Construire un AB A¬f pour la négation de f Il n‟accepte que les chaînes qui satisfont ¬f, qui violent f Calculer la composition synchrone des machines S et A¬f Contrôler si le langage accepté par cet automate est vide S‟il est vide, toutes les exécutions de S satisfont f S‟il a des exécutions, il y a au moins une exécution dans S qui est un contre-exemple pour f En pratique, la composition synchrone souvent n‟a pas besoin d‟être calculée dans sa totalité car dès qu‟on trouve un contre-exemple on a prouvé que l‟exigence n‟est pas satisfaite INF6001 Chap 7 47 Analyse de modèles, Model Checking byte n; proctype Aap() { do :: n++ :: noot!MIES od } Modèle M [] (n<3) Propriété Analyseur Espace d’états OUI Propriété satisfaite NON, + contre_exemple | M Explosion d‟états. INF6001 Chap 7 48 Définition[Clarke & Emerson 1981] “Model checking is an automated technique that, given a finite-state model of a system and a logical property, systematically checks whether this property holds for (a given initial state in) that model.” INF6001 Chap 7 49 Promela et SPIN Promela est un langage pour la spécification des systèmes répartis SPIN est l‟analyseur (model checker) et son point de départ est la théorie que nous venons de discuter INF6001 Chap 7 50 Promela Protocol/Process Meta Language Influencé par le CSP de Hoare Et par C Mais il est un langage pour la spécification de modèles Pas un langage d‟implantation De compréhension facile pour les implémenteurs Admet la communication Par variables globales partagées Synchrone, directe Asynchrone, par canaux INF6001 Chap 7 51 Promela Model A Promela model consist of: type declarations channel declarations global variable declarations process declarations [init process] behaviour of the processes: local variables + statements - simple vars - structured vars - vars can be accessed by all processes initialises variables and starts uploads/Industriel/ chap05-buchi 1 .pdf
Documents similaires










-
19
-
0
-
0
Licence et utilisation
Gratuit pour un usage personnel Attribution requise- Détails
- Publié le Jul 30, 2021
- Catégorie Industry / Industr...
- Langue French
- Taille du fichier 0.5223MB