Résumé:
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.
