Modélisation algorithmique et synthèse d'architectures assistées par model-checking

L'ingeenierie des architectures logicielles basee sur le prototypage rapide conduit a des iterations nombreuses dont le cout en simulation ne peut etre neeglige. Ceci se revele particulierement crucial pour les applications multimedia (encodeurs, decodeurs video, etc), qui cumulent des speci- cites de flux de donnees, de controle et de traitements complexes, decoupes en automates a grains fins. Les outils de modelisation HW/SW de telles applications sou ffrent donc d'une forme d'incompatibilite entre les ambitions en terme de prototypage et les besoins en tests incessants, consommateurs de temps. L'utilisation des techniques de veri fication formelle par "model-checking" constitue une solution a cette incompatibilite notoire. Nous decrivons dans cet article un travail exploratoire qui etudie l'association d'un outillage original de modelisation d'architectures mixtes logiciel materiel base sur le langage Ruby avec un outil de veri fication, nomme OBP (Observer-Based Prover), base sur les observateurs. Nous illustrons notre contribution par un exemple et decrivons des resultats sur les preuves d'exigences menees.