V rification Et Validation Formelles de Mod les UML

Cette thse s'intresse la problmatique de la vrification et de la validation (V&V) de modles UML. Notre objectif est de dterminer d'une part qu'un modle donn est bien form et cohrent, et d'autre part, qu'il satisfait les besoins des futurs utilisateurs du systme d'information. Dans ce contexte, nos principales contributions portent sur la proposition de deux approches pour la vrification et la validation formelles de modles UML. Ces deux approches sont ralises suite l'identification des relations inter-diagrammes UML, issues principalement du processus unifi UP et du mta-modle UML. La premire approche s'articule autour de la vrification de la cohrence d'un modle UML. Elle permet de rduire le nombre important d'oprations de vrification lmentaire en prservant la cohrence globale du modle. La deuxime approche propose une dmarche de validation des besoins des utilisateurs exprims sous forme de cas d'utilisation. L'objectif de cette approche consiste s'assurer que l'ensemble des besoins des utilisateurs, exprims par les diagrammes de cas d'utilisation documents, est totalement couvert par le diagramme d'activits tabli par l'expert de domaine.