[PDF] Cours de Model Checking - Leçon 2.1 : logiques temporelles

View - Download Cours de Model Checking - Leçon 2.1 : logiques temporelles

Previous PDF

Next PDF

RappelsIntuitionPr´eambuletechniqueLTL, CTL?, CTL

Comparaison

En bref

Cours de Model Checking

Le¸con 2.1 : logiques temporelles

S´ebastien Bardin

CEA-LIST, Laboratoire de Sˆuret´e Logicielle sebastien.bardin@cea.fr http://sebastien.bardin.free.fr/

S.BardinModel checking1/ 48

RappelsIntuitionPr´eambuletechniqueLTL, CTL?, CTL

Comparaison

En bref

Plan

Cours 2.1 : logiques temporelles

Rappel

Logiques temporelles : intuition

Pr´eambule technique

LTL, CTL?et CTL

Comparaison

Disgressions

Cours 2.2 : algorithmes

S.BardinModel checking2/ 48

Rappels

Intuition

Pr´eambule

technique

LTL, CTL?, CTL

Comparaison

En bref

Syst`emes r´eactifs

S.BardinModel checking3/ 48

Rappels

Intuition

Pr´eambule

technique

LTL, CTL?, CTL

Comparaison

En bref

Syst`emes r´eactifs II

Programme classique

termine retourne un r´esultat donn´ees complexes, contrˆole s´equentiel (≈simple) exemple : compilateur, algo de tri

Syst`eme r´eactif

ne doit pas terminer ne retourne pas de r´esultat donn´ees simples, contrˆole distribu´e (≈complexe) exemple : protocole, OS

S.BardinModel checking4/ 48

Rappels

Intuition

Pr´eambule

technique

LTL, CTL?, CTL

Comparaison

En bref

Syst`emes r´eactifs III

V´erifier un programme classique:Aspect temporel toujours identique, mais les pr´edicats sur les donn´ees peuvent ˆetre complexes. "Le programme termine et le tableau est tri´e".

S.BardinModel checking5/ 48

Rappels

Intuition

Pr´eambule

technique

LTL, CTL?, CTL

Comparaison

En bref

Syst`emes r´eactifs III

V´erifier un programme classique:Aspect temporel toujours identique, mais les pr´edicats sur les donn´ees peuvent ˆetre complexes. "Le programme termine et le tableau est tri´e". V´erifier un syst`eme r´eactif:Aspect temporel tr`es vari´e mais les pr´edicats sur les donn´ees sont souvent simples. "Si un processus demande infiniment souvent `a ˆetre ex´ecut´e, alors l"OS finira par l"ex´ecuter". "Il est toujours possible de revenir `a l"´etat initial". "Chaque fois qu"une panne est d´etect´ee, une alarme est ´emise". "Chaque fois qu"une alarme est ´emise, une panne a ´et´e d´etect´ee".

S.BardinModel checking5/ 48

Rappels

Intuition

Pr´eambule

technique

LTL, CTL?, CTL

Comparaison

En bref

Le model checking

Model Checking

Technique de v´erification automatique de syst`emes r´eactifs

Ingr´edients

M=syst`eme de transitions

?=formule temporelle

MC =est-ce queM |=??

Avantages

Phases amonts : sp´ecifs et design

Automatis´e

Trouve mieux les bugs que le test

Cost efficient(pour certains domaines)

S.BardinModel checking6/ 48

Rappels

Intuition

Pr´eambule

technique

LTL, CTL?, CTL

Comparaison

En bref

Syst`eme de transitions

Syst`eme de transitions = comportement du syst`eme r´eactif choicemoney cancel back served serving,0,trueserved,0,truemoney cancel idle,1,falseidle,2,falseidle,0,false

S.BardinModel checking7/ 48

Rappels

Intuition

Pr´eambule

technique

LTL, CTL?, CTL

Comparaison

En bref

Propri´et´es sur les syst`emes r´eactifs

Accessibilit´eUne certaine situation peut ˆetre atteinte xpeut valoir 0, toute instruction peut ˆetre ex´ecut´ee InvarianceChaque ´etat local respecte une bonne propri´et´e xne vaut jamais 0, le tableau ne d´eborde jamais Sˆuret´eQuelquechose de mauvais n"arrive jamais j"acc`ede au fichier uniquement si j"ai entr´e le bon PIN

Vivacit´eQuelquechose de bon finit par arriver

le programme termine, le message finit toujours par ˆetre transmis le programme revient toujours `a l"´etat initial ´Equit´eQuelquechose de bon se r´ep`ete infiniment souvent si un processus demande toujours la main, il l"aura infiniment

S.BardinModel checking8/ 48

Rappels

Intuition

Pr´eambule

technique

LTL, CTL?, CTL

Comparaison

En bref

Logiques temporelles

On exprimera les propri´et´es grˆace `a des logiques temporelles

A, E, F, G, U, X

Avantages

non ambigue g´en´erique ouvre la voie `a la v´erification automatique

Plusieurs logiques temporelles possibles

LTL, CTL, CTL?, ...

S.BardinModel checking9/ 48

Rappels

Intuition

Pr´eambule

technique

LTL, CTL?, CTL

Comparaison

En bref

La difficult´e du model checking

2 difficult´es principales

1.syst`eme de transitions fini

2.syst`eme de transitions suffisament petit

S.BardinModel checking10/ 48

Rappels

Intuition

Pr´eambule

technique

LTL, CTL?, CTL

Comparaison

En bref

La difficult´e du model checking

2 difficult´es principales

1.syst`eme de transitions fini

2.syst`eme de transitions suffisament petit

Syst`eme fini : probl`eme (parfois non trivial) de mod´elisation variables `a domaines finis, nombre born´e de tˆaches, etc.

S.BardinModel checking10/ 48

Rappels

Intuition

Pr´eambule

technique

LTL, CTL?, CTL

Comparaison

En bref

La difficult´e du model checking

2 difficult´es principales

1.syst`eme de transitions fini

2.syst`eme de transitions suffisament petit

Syst`eme fini : probl`eme (parfois non trivial) de mod´elisation variables `a domaines finis, nombre born´e de tˆaches, etc. Syst`eme petit : probl`eme algorithmique + mod´elisation

10 variables sur 8 bits : 10256possibilit´es

Stock´e une possibilit´e = 10 octets

Tout stocker≈10245To

S.BardinModel checking10/ 48

Rappels

Intuition

Pr´eambule

technique

LTL, CTL?, CTL

Comparaison

En bref

La difficult´e du model checking

2 difficult´es principales

1.syst`eme de transitions fini

2.syst`eme de transitions suffisament petit

Syst`eme fini : probl`eme (parfois non trivial) de mod´elisation variables `a domaines finis, nombre born´e de tˆaches, etc. Syst`eme petit : probl`eme algorithmique + mod´elisation

10 variables sur 8 bits : 10256possibilit´es

Stock´e une possibilit´e = 10 octets

Tout stocker≈10245To

Model Checking = g´erer l"explosion d"´etats

S.BardinModel checking10/ 48

Rappels

Intuition

Pr´eambule

technique

LTL, CTL?, CTL

Comparaison

En bref

En pratique

standard en v´erification de hardware (Intel, IBM, etc.) quelques beaux succ`es en software (drivers, fuzzing) It has been an exciting twenty years, which has seen the research focus evolve [...] from a dream of automatic program verification to a reality of computer-aided design debugging. - Thomas A. Henzinger (2001) Things like even software verification, this has been the Holy Grail of computer science for many decades but now in some very key areas, for example, driver verification we"re building tools that can do actual proof about the software and how it works in order to guarantee the reliability. - Bill Gates (2002)

S.BardinModel checking11/ 48

Rappels

Intuition

Pr´eambule

technique

LTL, CTL?, CTL

Comparaison

En bref

Historique

1975Constat : v´erif. inadapt´ee `a syst`emes r´eactifs

1977Pnueli propose d"utiliser les logiques temporelles

1981Model checking de CTL par Clarke et al., Sifakis et al.

1980-1990Nombreux r´esultats th´eoriques

1990-2000´Enorme am´elioration des performancesExtensions : proba, temps, infini

2000-...MC adopt´e par les principaux fondeurs (Intel, etc.)Standardisation du langage temporel PSLD´ebuts du software model checking (Microsoft)Prix ACM Paris Kanellakis Award 1998 et 2005

2008Prix Turing d´ecern´e `a Clarke, Sifakis et Emerson

S.BardinModel checking12/ 48

Rappels

Intuition

Pr´eambule

technique

LTL, CTL?, CTL

Comparaison

En bref

Bibliographie

Livres

Principles of Model Checking [Baier-Kaoten 08]

Model Checking [Clarke-Grumberg-Peled 99]

V´erification de logiciels [LSV 99]

S.BardinModel checking13/ 48

Rappels

Intuition

Pr´eambule

technique

LTL, CTL?, CTL

Comparaison

En bref

Plan

Rappel

Logiques temporelles : intuition

Pr´eambule technique

LTL, CTL?et CTL

Comparaison

Disgressions

S.BardinModel checking14/ 48

Rappels

Intuition

Pr´eambule

technique

LTL, CTL?, CTL

Comparaison

En bref

Exprimer des propri´et´es temporelles

Besoin d"exprimer des familles de propri´et´es et pas juste quelques cas particuliers

Langages naturels

impr´ecis (donc pas d"automatisation) verbeux

Formalismes graphiques

plus pr´ecis concis faciles `a apprendre et `a communiquer manque d"expressivit´e ou/et de pr´ecision

S.BardinModel checking15/ 48

Rappels

Intuition

Pr´eambule

technique

LTL, CTL?, CTL

Comparaison

En bref

Exprimer des propri´et´es temporelles

Besoin d"exprimer des familles de propri´et´es et pas juste quelques cas particuliers

Langages naturels

impr´ecis (donc pas d"automatisation) verbeux

Formalismes graphiques

quotesdbs_dbs31.pdfusesText_37

[PDF] deshalb place du verbe

[PDF] namlich

[PDF] construction phrase allemand

[PDF] vocabulaire allemand bac

[PDF] mots de liaison anglais exercice

[PDF] exercices mots de liaison anglais pdf

[PDF] conjonction de subordination anglais pdf

[PDF] mots de liaison anglais toeic

[PDF] mot de vocabulaire espagnol

[PDF] connecteurs logiques liste

[PDF] les connecteurs logiques en français exercices

[PDF] les connecteurs logiques exercices cm2

[PDF] exemple de texte avec connecteur logique

[PDF] les connecteurs logiques en français exercices pdf

[PDF] exercices connecteurs temporels ce2