Remerciez-le!

Remerciez @Admin pour avoir partagé cet document gratuitement, de la manière la plus simple, en partageant sur les réseaux sociaux.

Chap05 buchi Chapitre Véri ?cation de modèles Automates de Büchi et SPIN Holzmann Chap Chap http w uqo ca luigi INF CPropriétés d ? états et exécutions cha? nes X X X s X X X s s s X ? Nous pouvons a ?rmer des propriétés pour X entier et a résultat entier

Chapitre Véri ?cation de modèles Automates de Büchi et SPIN Holzmann Chap Chap http w uqo ca luigi INF CPropriétés d ? états et exécutions cha? nes X X X s X X X s s s X ? Nous pouvons a ?rmer des propriétés pour X entier et a résultat entier Des états p ex à l ? état s X toujours invariant pas besoin de logique temporelle ici Des exécutions p ex x ? ou ? x ? mais pas ? x ? Observez que dans ce cas le contrôle est sur les transitions INF Chap État d ? acc eptation CComment véri ?er 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éri ?e ces propriétés ?? composition synchrone ? nous pouvons aussi véri ?er une propriété négative c -à -d que la machine ne satisfait pas une propriété ? never automata INF Chap CVéri ?cation de modèle Modèle à véri ?er Machine exprimant des propriétés à véri ?er Composition synchrone INF Chap CExemple AB pour véri ?er ?p p s Cet AB synchronise avec un autre AB seulement si la propriété p reste toujours vraie à toutes les transitions INF Chap CAcceptation dans les automates de Büchi ? Un automate régulier accepte toutes les cha? nes qui conduisent à un état ?nal ? Un AB accepte toutes les cha? nes in ?nies qui passent un nombre in ?ni de fois par un état ?nal ? 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 e ?ectuer cette construction pas discuté dans ce cours CIncomplétude des AB ? L ? AB de gauche ne considère pas le cas de recevoir un ? p ? Ceci simpli ?e la compréhension et la véri ?cation car les transitions qui ne conduisent pas au résultat désiré ne sont pas prises en considération p p s s s ? p INF Chap CExemple AB pour véri ?er p ? p true s p s Cet AB est prêt à accepter des transitions o? p est faux mais il est content seulement quand p devient vrai INF Chap CExemple ?p AB pour véri ?er que en ?n toujours p true p s p s ? true ? accepte p et autres mais après un certain p il n ? accepte que des p après INF Chap CComparer avec AB déterministe L ? AB ci-dessous n ? est pas bon pour ?p Car s ? il y a un er p qui n ? est pas suivi par ?p il rejette Il faut dans ce cas continuer à chercher un p futur après lequel ?p p p s p s Cet AB montre aussi les limites de l ?