Abstract FR:

Les travaux presentes dans cette these s'inscrivent dans les cadre des methodologies de conception materiel/logiciel. Traditionnellement, la conception conjointe est divisee en deux grandes parties : la cospecification, qui correspond a la specification du systeme sans a priori sur l'implantation finale, et le partitionnement, qui correspond au choix de la realisation - materiel et/ou logiciel - des differentes fonctionnalites du systeme. Dans cette these, nous presentons un nouveau formalisme de specifications dynamiques temps reel offrant la possibilite de prendre en compte les aspects temps reel au niveau de l'etape de cospecification. Cette apport est important puisque l'etape de partitionnement utilise de maniere intensive les facteurs temps reel pour proposer une solution au decoupage logiciel-materiel. Ce formalisme permet de prendre en compte les aspects dynamiques d'un systeme et d'exprimer des contraintes temps reel - sur les dates et les durees d'execution associees aux operations utilisees pour specifier un systeme. A la difference des approches de type algebriques existantes, le formalisme que nous presentons ne fait pas appel a une logique externe temps reel pour prendre en compte les aspects temps reel, mais fournit un cadre dans lequel les contraintes temps reel et les autres proprietes du systeme sont exprimees de maniere homogene. De plus, ce formalisme n'utilise qu'un nombre restreint de primitives dediees a la manipulation du temps, ce qui rend l'expression des contraintes temps reel relativement simple et intuitive et donc plus claire et lisible. Nous utilisons, ensuite, notre formalisme pour donner une semantique axiomatique a un sous-ensemble de vhdl. La semantique que nous proposons est une semantique orientee utilisateur. L'avantage d'une telle approche est que cela permet de s'abstraire, autant que possible, de toutes notions d'implantation relatives au simulateur, ce qui est compatible avec l'objectif de la cospecification. Nous montrons que l'on peut alors extraire d'un code vhdl des specifications dans notre formalisme temps reel, ce qui permet de retablir, entre l'etape de cospecification et l'etape de partitionnement, un flot formel. Ces travaux illustrent le fait que l'utilisation des methodes formelles ne saurait se reduire a l'etape de specifications avant partitionnement, et fournissent un moyen d'etendre la portee de telles approches.