Abstract FR:

Nous apportons une contribution a l'elaboration de methodes de developpement de logiciels embarques unissant a la fois une methode structuree en l'occurence sa-rt selon hatley et pirbhai et une methode formelle (le modele des systemes de transitions etiquetes). Nous decrivons comment le formalisme des systemes de transitions etiquetes pour fournir une semantique formelle pour les diagrammes de flots de donnees et de flots de controle, assortis de la specification de controle associee. Nous presentons ensuite le programme developpe qui automatise cette transformation et quelques possibilites de verifications sur ce modele grace a l'outil mec. Une comparaison est ensuite faite avec une autre approche consistant a specifier directement le systeme en termes de produits de systemes de transitions etiquetes, et les conclusions en sont titees