Spécification et vérification formelle de la sécurité D’une Architecture à base de réseau sans fil orientée NoC

Abstract

Les syst ` emes embarques ont un fort impact dans la vie quotidienne par exemple ,les syst ` emes comme les t ´ el ´ eviseurs,les t ´ el ´ ephone cellutaires,cartes de cr ´ edits sont utilis ´ ee pour les personnes,tandis que d’autres syst ` emes ,comme les r ´ eseaux,les t ´ el ´ ecommunication,la distribution et int ´ egr ´ es dispositifs,les super ordinateurs sont utilis ´ ee par des organisation telles que les entreprise,les gouvernements,les nations....Plusieurs pays,basant sur syst ` eme MPSOc ` a base de NoC,Ces syst ` emes doivent ˆ etre fiable,et leurs sp ´ ecifications et la conception doivent ˆ etre claire ,compr ´ ehensibles et doivent des r ` egles pr ´ ecises et ils doivent ´ eviter les d ´ efauts, les ´ echecs et s’ils ne peuvent pas ,ils devraient au moins ˆ etre tol ´ erant aux pannes et de s ´ ecurit ´ e ,par cons ´ equent en raison de ces exigences,”V ´ erification formelle ” peut ˆ etre utile pour obtenir une assurance et la garantie de leur exactitude par rapport aux questions de suret ´ e et de s ´ ecurit ´ e.Event-B est d ´ efinie comme une m ´ ethode de d ´ eveloppement formelle mettant en valeur aussi bien les aspects statiques que dynamiques d’un syst ` eme Tirant comme un cas d’ ´ etude le syst ` eme multi-nœud sans fil qui repr ´ esente un syst ` eme distribu ´ e int ´ egrant MPSoC en r ´ eseau sur puce (NOC) permet de communique gr ˆ ace ` a la communication ZigBee.Dans ce travail nous proposons de sp ´ ecifier et prouver formellement ce type de syst ` eme en instanciant un mod ` ele bas ´ e sur graphe color ´ es,le langage de description utilis ´ e est Event-B qui s’appuie sur l’outils Rodin.Cette description permet d’am ´ elior ´ e la sp ´ ecification en vue d’augmenter les performances d’une solution de fiabilit ´ e auto-organis ´ ee bas ´ e sur les MPSoC sans fil multi- nœud Mots-Cles :Systemes Embarques,Methode formelles ,B-Event ,NoC ,Reseau sans fil ,Algorithme de coloration de graphes.