Remerciez-le!

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

Introduction au Model Checking S´ ebastien Bardin CEA,LIST, Laboratoire de Sˆ u

Introduction au Model Checking S´ ebastien Bardin CEA,LIST, Laboratoire de Sˆ uret´ e logicielle Gif-sur-Yvette, F-91191 France sebastien.bardin@cea.fr Table des mati` eres 1 Introduction 2 1.1 Syst` emes r´ eactifs . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 2 1.2 Propri´ et´ es temporelles . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 2 1.3 Model checking . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 3 1.4 Historique . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 3 1.5 En pratique . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 4 1.6 Lectures conseill´ ees . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 6 I Bases du model checking 7 2 Mod´ elisation des syst` emes r´ eactifs 8 2.1 Syntaxe : machines ` a ´ etats . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 8 2.2 S´ emantique : syst` emes de transitions . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 8 2.3 Structure de Kripke . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 10 2.4 Discussion sur la terminologie . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 12 2.5 Espace des ´ etats, propri´ et´ es d’accessibilit´ e et d’invariance . . . . . . . . . . . . . . . . . . . . 12 2.6 Syst` emes concurrents . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 14 2.7 Hypoth` eses d’´ equit´ e . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 15 2.8 Propri´ et´ es de sˆ uret´ e. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 16 2.9 Quelques points de mod´ elisation . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 17 3 Logiques temporelles 19 3.1 Panorama de propri´ et´ es temporelles . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 19 3.2 Intuitions sur les logiques temporelles . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 20 3.3 Logique lin´ eaire LTL . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 24 3.4 Logique branchante CTL∗. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 26 3.5 Logique branchante CTL . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 27 3.6 Comparaison des trois logiques . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 4 Model checking, algorithmes de base 31 4.1 Pr´ elude : composantes fortement connexes . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 4.2 Model checking de CTL par labelling . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 4.3 Model checking de fair CTL par labelling . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 4.4 Model checking de LTL par automates . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 R´ ef´ erences 38 1 A Rappels de logique 40 A.1 D´ eﬁnitions . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 40 A.2 Probl` emes classiques li´ es aux logiques . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 40 A.3 Quelques logiques . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 41 A.4 Exemple : logique classique propositionnelle . . . . . . . . . . . . . . . . . . . . . . . . . . . . 41 B Notions de calculabilit´ e et complexit´ e 43 B.1 Calculabilit´ e . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 43 B.2 Complexit´ e . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 44 C Divers probl` emes algorithmiques 45 C.1 Composantes fortement connexes . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 45 D Sujets de partiel 47 D.1 ENSTA, ann´ ee 2006-2007 . . . . . . . . . . . . . uploads/Philosophie/ mc-saclay-poly.pdf