Réécriture d'un modèle MCSE à l'aide du langage FIACRE

Le travail presente dans ce document s'inscrit dans une demarche de conception des systemes embarques. Il se focalise sur les regles de reecriture d'un modele exprime en MCSE dans le langage FIACRE. Cette reecriture vise a permettre une verification formelle des proprietes du modele tout en garantissant le respect de la semantique du langage de haut-niveau MCSE. Les regles exposees couvrent la totalite de l'expressivite du modele d'entree et sont illustrees sur des exemples simples.