MASTER RECHERCHE EN INFORMATIQUE

Naim Aber

Description

Niveau: Supérieur, Master

• rapport de stage

Rapport de Stage MASTER RECHERCHE EN INFORMATIQUE Specialite : COSY : des COncepts aux SYstemes Sujet : Verification d'un protocole Stop-And-Wait : Combiner Model-Checking et Preuve de theoremes par : Naim ABER Stage d'initiation a la recherche e?ectue au Laboratoire d'Informtique de Paris Nord au sein de l'equipe Logique, Calcul et Raisonnement, UMR 7030 du CNRS Sous la direction de : M. Kais Klai : Maıtre de conferences a UP13 - LIPN - LCR Mme. Micaela Mayero : Maıtre de conferences a UP13 - LIPN - LCR Annee universitaire 2008-2009

• modele


• modele cpn-ami du protocole swp


• cpn


• protocole


• principes des protocoles de la couche liaison de donnees


• reseau de petri


• formalisation du protocole

Sujets

• Modèle
• Protocole
• Réseau de Petri
• rapport de stage
• rapport de stage master

Informations

• Publié par: cidur
• Nombre de lectures: 434

Extrait

Rapport de Stage MASTER RECHERCHE EN INFORMATIQUE Specialite:  COSY:desCOnceptsauxSYstemes

Sujet : Vericationd'unprotocoleStop-And-Wait: CombinerModel-CheckingetPreuvedetheoremes

par : Naim ABER

Staged'initiationalarechercheeectueauLaboratoire d'Informtique deParisNord au seindel'equipeLogique,Calcul etRaisonnement, UMR 7030 du CNRS

Sous la direction de : M.KaisKlai:Ma^tredeconferencesaUP13-LIPN-LCR Mme.MicaelaMayero:Ma^tredeconferencesaUP13-LIPN-LCR

Anneeuniversitaire2008-2009

TabledesMatieres

Table des Figures

Liste des tableaux

INTRODUCTION GENERALE

Tabledesmatieres

i

iv

1

2

1 Approches de verication formelle 5  1.1 Introduction . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 5 1.2Approchesdevericationformelle.......................6 1.2.1 Model checking . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 6 1.2.1.1Presentation.........................6 1.2.1.2ReseauxdePetri.......................7 1.2.1.3ReseauxdePetricolores...................9 1.2.1.4OutilsdedeveloppementdesreseauxdePetri.......10 1.2.2Preuvesdetheoremes..........................11 1.2.2.1Presentation.........................11 1.2.2.2Denitions..........................11 1.2.2.3 Assistants de preuve . . . . . . . . . . . . . . . . . . . . . 12 1.3 Conclusion . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 13  2 Etude de cas : le protocole "Stop and Wait" 14 2.1 Introduction . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 14 2.2PrincipesdesprotocolesdelacoucheLiaisondedonnees..........15 2.3 Description du Protocole "Stop and Wait" . . . . . . . . . . . . . . . . . . 16

i

2.4Informationsdecontr^ole............................17 2.5 Conclusion . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 18 3Modelisationetvericationduprotocole"StopandWait"avecCPN- AMI 19 3.1 Introduction . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 19 3.2 Environnement CPN-AMI . . . . . . . . . . . . . . . . . . . . . . . . . . . 19 3.3Modelisationduprotocole"StopandWait"avecCPN-AMI........20 3.3.1Declarations...............................20 3.3.2Placesettransitionsdumodele....................21 3.3.3 Description du modele . . . . . . . . . . . . . . . . . . . . . . . . . 22  3.4Analysedumodeleetvericationdeproprietes...............23 3.4.1Vericationsyntaxique.........................23 3.4.2 Bornes de places . . . . . . . . . . . . . . . . . . . . . . . . . . . . 23 3.5Modeleavecunnombrenideretransmissions................24 3.5.1Vericationsyntaxique.........................25 3.5.2 Bornes de places . . . . . . . . . . . . . . . . . . . . . . . . . . . . 26 3.5.3Graphedesetatsaccessibles......................26 3.5.4 Duplication . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 27 3.6 Conclusion . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 27 4 Formalisation du protocole "Stop and Wait" en Coq 29 4.1 Introduction . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 4.2 Assistant de preuve Coq . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 4.3 Formalisation du protocole "Stop and Wait" en Coq . . . . . . . . . . . . . 30 4.3.1Formalisationdel'aspectstatiquedureseau.............31 4.3.2Formalisationdel'aspectdynamiquedumodele...........35 4.3.2.1 Gardes . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 4.3.2.2Miseajourdumarquagecourant..............36 4.3.2.3Franchissabilite........................40 4.3.2.4 Franchissement d'une transition . . . . . . . . . . . . . . . 42 4.4 Conclusion . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 46

CONCLUSION

Bibliographie

  GENERALE

47

49

1.1 1.2

2.1 2.2

3.1 3.2 3.3 3.4 3.5 3.6 3.7

4.1 4.2

Table des gures

Exempled'unreseaudePetri.........................8 Exempled'unreseaudePetricolore......................9

PileprotocolairedumodeleOSI........................15 Informationsdecontr^oleduprotocole"StopandWait"..........18 .

ModeleCPN-AMiduprotocoleStopandWait................20 Informationsstatistiquessurlemodele....................23 Bornes de places . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 24 ModeleCPN-AMiduprotocoleStopandWaitavecunnombrenide retransmissions . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 25 Vericationsyntaxique.............................26 Bornes de places . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 26 Bornes de la placemsg recieved. . . . . . . . . . . . . . . . . . . . . . . . 27

ModeleCPN-AMiduprotocoleSWP.....................31 Exempledefranchissementd'unetransitiondansunreseaudePetricolore35

iv

3.1

3.2

3.3

3.4

Liste des tableaux

 Places et transitions de l'Emetteur . . . . . . . . . . . . . . . . . . . . . .

PlacesettransitionsduRecepteur.......................

PlacesettransitionsduReseau........................

GraphedesetatsaccessiblesenfonctiondunombrederetransmissionsR

1

.

21

21

22

27

  INTRODUCTION GENERALE

Contextescientiqueetproblematique

Denosjours,lessystemesinformatiquestempsreelsontpresentsdansdemultiplessec- teursd'activites:contro^ledessystemesautomatisesdeproduction,aidealaconduitedes vehicules(enparticulierdansledomainedel'aviation)ougestiondesuxd'information surdesreseauxlocauxetsurInternet.Aucoursdesdernieresannees,lessystemestemps reelsesontprogressivementetabliscommeunedisciplineapartentierequirassembleune fortecommunauteissuealafoisdumondeacademiqueetdel'industrie.L'evolutionde cessystemessecaracteriseparunecomplexitecroissanteetunro^letoujourspluscritique. Leursmiseaupointestunproblemecomplexepourlequelilestrecommanded'utiliser des techniques de : 1)Descriptionformelleandespeciersansambigutelecomportementdesapplications considerees. 2) V ication formelle an de valider le bon fonctionnement de ces applications. La er vericationformelleconsisteas'assurerdelacorrectiond'unprogrammeouunlogiciel, parrapportadesproprietesellesaussideniesformellement.

Dierentesapprochesmathematiquesonteteutiliselaborerdesraisonnements ees pour formelssurcessystemes,parmilesquellesoncitenotamment: {Lemodelchecking[1]:consisteaanalyserexhaustivementl'evolutiondusysteme lorsdesesexecutionspossibles.Parexemple,pourdemontrerl'absenced'erreursa l'execution,onpourratesterl'absenced'etatsd'erreurdansl'ensembledesetatsac- cessiblesdusysteme.Ils'agitalorsd'uneformedetest(informatique)exhaustif,mais meneal'aided'algorithmesastucieuxpermettantd'enumererlesetatsdusysteme sousuneformesymbolique(c'est-a-direeconomiqueentermed'espacememoire). {Lapreuvedetheoreme[4]:tendademontrerdestheoremessurlesformuleslogiques decrivantlasemantiqueduprogrammeal'aided'outilslogicielsappelesassistants depreuve.Cesoutilspermettental'utilisateurdedemontrerdestheoremessurle programme,avecuneaideetunevericationparlamachine.

2