UML subit des reproches incessants sur le manque de ses fondements formels. L'imprecision de sa semantique complique la verification des modeles quand la correction des specifications devient une condition incontournable en genie logiciel. Reconnues pour leurs fondements theoriques rigoureux, les langages formels sont a meme de repondre a ce besoin. Ils sont toutefois peu utilises en raison de leur complexite. Aussi, pour rallier convivialite et rigueur, de nombreuses equipes de recherches s'activent autour de la semantique d'UML dans le but de lui conferer des bases solidement construites. La principale motivation de cette etude a ete, tout le long de son developpement, de parvenir a une modelisation UML valide sans obligation de maitrise, pour le concepteur UML, des techniques formelles usitees en pareille situation. Cet objectif, plutot ambitieux, ouvre de larges horizons sur la semantique des langages et l'analyse des modeles qui en decoulent. La methodologie que nous proposons apporte plusieurs contributions. Sa principale originalite apparait dans le large spectre de diagrammes qu'elle integre, de facon complementaire, pour produire un modele unique formellement verifie."