UML subit des reproches incessants sur le manque de ses fondements formels. L'imprcision de sa smantique complique la vrification des modles quand la correction des spcifications devient une condition incontournable en gnie logiciel. Reconnues pour leurs fondements thoriques rigoureux, les langages formels sont  mme de rpondre  ce besoin. Ils sont toutefois peu utiliss en raison de leur complexit. Aussi, pour rallier convivialit et rigueur, de nombreuses quipes de recherches s'activent autour de la smantique d'UML dans le but de lui confrer des bases solidement construites. La principale motivation de cette tude a t, tout le long de son dveloppement, de parvenir  une modlisation UML valide sans obligation de matrise, pour le concepteur UML, des techniques formelles usites en pareille situation. Cet objectif, plutt ambitieux, ouvre de larges horizons sur la smantique des langages et l'analyse des modles qui en dcoulent. La mthodologie que nous proposons apporte plusieurs contributions. Sa principale originalit apparat dans le large spectre de diagrammes qu'elle intgre, de faon complmentaire, pour produire un modle unique formellement vrifi.