[PDF] Cours de Model Checking - Leçon 2 : Logiques temporelles

View - Download Cours de Model Checking - Leçon 2 : Logiques temporelles

Previous PDF

Next PDF

IntroductionKripkeBases de logiqueLTLCTL?

CTL

Comparaison

En bref

Cours de Model Checking

Le¸con 2 : 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/ 44

Introduction

Kripke

Bases de logique

LTL CTL? CTL

Comparaison

En bref

Rappels

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 |=??

Vu au dernier cours

mod´elisation calcul de l"espace des ´etats accessibilit´e, invariance, sˆuret´e

S.BardinModel checking2/ 44

Introduction

Kripke

Bases de logique

LTL CTL? CTL

Comparaison

En bref

Types de propri´et´es temporelles

Accessibilit´e

Une certaine situation peut ˆetre atteinte

Invariance

Tous les ´etats du syst`eme satisfont une bonne propri´et´e

Sˆuret´e

Quelquechose de mauvais n"arrive jamais

Vivacit´e

Quelquechose de bon finit par arriver

´Equit´e

Quelquechose de bon se r´ep`ete infiniment

´Equivalence comportementale

Est-ce que 2 syst`emes sont ´equivalents ?

S.BardinModel checking3/ 44

Introduction

Kripke

Bases de logique

LTL CTL? CTL

Comparaison

En bref

Types de propri´et´es temporelles

Accessibilit´e

Une certaine situation peut ˆetre atteinte

Invariance

Tous les ´etats du syst`eme satisfont une bonne propri´et´e

Sˆuret´e

Quelquechose de mauvais n"arrive jamais

Vivacit´e

Quelquechose de bon finit par arriver

´Equit´e

Quelquechose de bon se r´ep`ete infiniment

´Equivalence comportementale

Est-ce que 2 syst`emes sont ´equivalents ?

S.BardinModel checking3/ 44

Introduction

Kripke

Bases de logique

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 checking4/ 44

Introduction

Kripke

Bases de logique

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

On se tourne vers des sp´ecifications logiques

S.BardinModel checking4/ 44

Introduction

Kripke

Bases de logique

LTL CTL? CTL

Comparaison

En bref

Logiques temporelles

Pourquoi des logiques ?

exprimer sans ambiguit´e les propri´et´es attendues prouver la correction du syst`eme

Logique temporelle

logique classique + op´erateurs d´edi´es au temps connecteurs temporels + quantificateurs de chemins

Pourquoi des logiques temporelles ?

concision, expressivit´e, simplicit´e algorithmique : d´ecision et complexit´e

S.BardinModel checking5/ 44

Introduction

Kripke

Bases de logique

LTL CTL? CTL

Comparaison

En bref

Logiques temporelles

Pourquoi des logiques ?

exprimer sans ambiguit´e les propri´et´es attendues prouver la correction du syst`eme

Logique temporelle

logique classique + op´erateurs d´edi´es au temps connecteurs temporels + quantificateurs de chemins

Pourquoi des logiques temporelles ?

concision, expressivit´e, simplicit´e algorithmique : d´ecision et complexit´e

Attention

Temporel versus Temporis´e

S.BardinModel checking5/ 44

Introduction

Kripke

Bases de logique

LTL CTL? CTL

Comparaison

En bref

Logiques temporelles II

Deux sortes d"op´erateurs d´edi´es au temps

Connecteurs temporels: sur un chemin

suite d"´ev`enements attendusle long d"un seul chemin nous verrons entre autreU,X,G,F insuffisant : en g´en´eral on veut savoir si tout ou partie des chemins partant d"un ´etat donn´e v´erifient une propri´et´e Quantificateurs de chemin: sur un (d´epliage du) syst`eme de transition quantifie les chemins partant d"un ´etat qui doivent v´erifierla propri´et´e nous verronsA,E

S.BardinModel checking6/ 44

Introduction

Kripke

Bases de logique

LTL CTL? CTL

Comparaison

En bref

Connecteurs temporels

Exprimer le s´equencement d"´ev`enements le long d"un chemin

Op´erateurX"next"

Xpp

S.BardinModel checking7/ 44

Introduction

Kripke

Bases de logique

LTL CTL? CTL

Comparaison

En bref

Connecteurs temporels

Exprimer le s´equencement d"´ev`enements le long d"un chemin

Op´erateurF"sometimes in the future"

Fpp

S.BardinModel checking7/ 44

Introduction

Kripke

Bases de logique

LTL CTL? CTL

Comparaison

En bref

Connecteurs temporels

Exprimer le s´equencement d"´ev`enements le long d"un chemin

Op´erateurG"always in the future"

Gp,ppppppp p

S.BardinModel checking7/ 44

Introduction

Kripke

Bases de logique

LTL CTL? CTL

Comparaison

En bref

Connecteurs temporels

Exprimer le s´equencement d"´ev`enements le long d"un chemin

Op´erateurU"p true until q true"

pUq,ppppppq

S.BardinModel checking7/ 44

Introduction

Kripke

Bases de logique

LTL CTL? CTL

Comparaison

En bref

Connecteurs temporels

Exprimer le s´equencement d"´ev`enements le long d"un chemin Xpp Fpp

Gp,ppppppp p

pUq,ppppppq

S.BardinModel checking7/ 44

Introduction

Kripke

Bases de logique

LTL CTL? CTL

Comparaison

En bref

Connecteurs temporels II

Exemples pour un seul chemin

Accessibilit´e :F(x= 0)

Invariance :G¬(x= 0)

Vivacit´e :G(p→Fq)

Correction totale :

S.BardinModel checking8/ 44

Introduction

Kripke

Bases de logique

LTL CTL? CTL

Comparaison

En bref

Quantificateurs de chemin

Les connecteurs temporels :

consid`erent une ex´ecution `a la fois ex´ecutions ind´ependantes les unes des autres ex´ecutions organis´ees en un ensemblequotesdbs_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