Remerciez-le!

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

Mc saclay poly Introduction au Model Checking S ?ebastien Bardin CEA LIST Laboratoire de Su ret ?e logicielle Gif-sur-Yvette F- France sebastien bardin cea fr CTable des mati eres Introduction Syst emes r ?eactifs Propri ?et ?es temporelles Model checking

Introduction au Model Checking S ?ebastien Bardin CEA LIST Laboratoire de Su ret ?e logicielle Gif-sur-Yvette F- France sebastien bardin cea fr CTable des mati eres Introduction Syst emes r ?eactifs Propri ?et ?es temporelles Model checking Historique En pratique Lectures conseill ?ees I Bases du model checking Mod ?elisation des syst emes r ?eactifs Syntaxe machines a ?etats S ?emantique syst emes de transitions Structure de Kripke Discussion sur la terminologie Espace des ?etats propri ?et ?es d ? accessibilit ?e et d ? invariance Syst emes concurrents Hypoth eses d ? ?equit ?e Propri ?et ?es de su ret ?e Quelques points de mod ?elisation Logiques temporelles Panorama de propri ?et ?es temporelles Intuitions sur les logiques temporelles Logique lin ?eaire LTL Logique branchante CTL ? Logique branchante CTL Comparaison des trois logiques Model checking algorithmes de base Pr ?elude composantes fortement connexes Model checking de CTL par labelling Model checking de fair CTL par labelling Model checking de LTL par automates R ?ef ?erences CA Rappels de logique A D ?e ?nitions A Probl emes classiques li ?es aux logiques A Quelques logiques A Exemple logique classique propositionnelle B Notions de calculabilit ?e et complexit ?e B Calculabilit ?e B Complexit ?e C Divers probl emes algorithmiques C Composantes fortement connexes D Sujets de partiel D ENSTA ann ?ee - D ENSTA rattrapages ann ?ee - CChapitre Introduction Systemes r ?eactifs Habituellement un programme que nous dirons standard termine retourne un r ?esultat et manipule des donn ?ees complexes mais sa structure de contr ole est assez simple Pour ces programmes standards les propri ?et ?es a prouver sont toujours du style ??quand la fonction est appell ?ee et que la pr ?econdition est v ?eri ? ?ee alors la fonction termine et la postcondition est v ?eri ? ?ee ? Exemple typique de programme standard compilateur algorithme de tri Ici nous nous int ?eressons a une classe tres particuliere de programmes les systemes r ?eactifs Quelques propri ?et ?es remarquables de ces systemes ils ne terminent pas forc ?ement ils ne calculent pas un r ?esultat mais pluto t maintiennent une interaction les types de donn ?ees manipul ?es sont souvent simples alors que le contr ole est complexe ex ?ecution de plusieurs composants en parallele En ?n bien souvent ils interagissent avec un environnement par le biais de capteurs prise d ? information et d ? actionneurs action Exemples typiques de systemes r ?eactifs systemes embarqu ?es pour les transports l ? ?energie systemes d ? exploitation protocoles de communication etc Propri ?et ?es temporelles Les propri ?et ?es que l ? on veut prouver sur ces systemes r ?eactifs sont tres di ? ?erentes de celles que l ? on veut prouver sur des programmes standards On veut typiquement prouver des propri ?et ?es sur l ? entrelacement des ?evenements tout au long de l ? ex ?ecution in ?nie du programme par exemple ?? si un processus demande in ?niment souvent a etre