Description
Date depot: 1 janvier 1900
Titre: Vérification formelle des diagrammes dynamiques UML2 : Applications aux systèmes Temps-Réels Embarqués.
Directeur de thèse:
Kamel BARKAOUI (CEDRIC)
Domaine scientifique: Sciences et technologies de l'information et de la communication
Thématique CNRS : Non defini
Resumé:
Le manque de sémantique du langage de modélisation UML (Unified Modeling langage) est souvent invoqué comme atout à la vulgarisation de la notation favorisant sa large utilisation, la correction de la modélisation requiert en revanche une sémantique formelle rigoureusement définie.
Dans ce sens, UML2.0 apporte plus de précisions à UML1.x mais la notation reste informelle et manque d'outils pour l'analyse et la vérification automatique des modèles.
Dans un premier temps, le travail de thèse devra commencer par l'étude détaillée de la sémantique des différents diagrammes dynamiques (diagrammes d’interactions (séquence, collaboration) diagramme d’activité, diagramme de cas d’utilisation) afin de bien cerner leurs insuffisances révélées lors de l'élaboration d'UML2.0 y compris les extensions proposées pour décrire les exigences temporelles.
Dans un second temps, nous devrons proposer un ou plusieurs formalismes (basé sur les réseaux de Pétri temporisé ou autre) capables de doter les diagrammes UML d’une sémantique formelle permettant ainsi de mener une vérification aussi bien qualitative que quantitative.
Enfin, nous chercherons à valider l'approche développée sur les systèmes Temps-Réels Embarqués, pour s'assurer de leur bon fonctionnement logique ou temporel à travers une application significative.
Doctorant.e: Louati Aymen