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érifierp 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

  • 19
  • 0
  • 0
Afficher les détails des licences
Licence et utilisation
Gratuit pour un usage personnel Attribution requise
Partager