Abstract FR:

Le langage UML est largement utilisé pour décrire la dynamique des systèmes. Il propose les diagrammes de séquence (DS) pour décrire les interactions entre les objets d'un système et les diagrammes d'états-transitions (DET) pour décrire le comportement de ces objets. Ce langage a attiré l'attention de ses utilisateurs pour dériver les DET des objets à partir de leurs interactions. Cependant, il manque d'une sémantique formelle et donc ne propose pas de liens sémantiques entre ces diagrammes de la dynamique. En particulier, les DS ne disposent pas d'une sémantique opérationnelle définissant formellement comment ils s'exécutent. Par conséquent, il n'est pas possible de dériver formellement des DET à partir des DS. L'objectif principal de cette thèse est de formaliser les DS UML. Ainsi, il sera possible de dériver à partir d'un ensemble de DS les DET des objets participant à ces DS. Nos contributions principales dans cette thèse sont : (i) doter les DS d'une sémantique opérationnelle. Nous avons proposé quatre sémantiques, chacune est décrite sous la forme d'une relation d'ordre partiel entre les événements d'émission et de réception des messages. (ii) Dériver à partir d'une spécification exprimée par un ensemble de DS les DET des objets participent à ces DS. (iii) Détecter la présence de nouvelles interactions n'appartenant pas à la spécification de départ, mais impliquées par l'interaction des objets.